functor (M : Memory.Model) ->
sig
type logic = M.loc Memory.logic
val value : Cvalues.Logic.logic -> Lang.F.term
val loc : Cvalues.Logic.logic -> M.loc
val vset : Cvalues.Logic.logic -> Vset.set
val sloc : Cvalues.Logic.logic -> M.loc Memory.sloc list
val rdescr : M.loc Memory.sloc -> Lang.F.var list * M.loc * Lang.F.pred
val map : Lang.F.unop -> Cvalues.Logic.logic -> Cvalues.Logic.logic
val map_opp : Cvalues.Logic.logic -> Cvalues.Logic.logic
val map_loc :
(M.loc -> M.loc) -> Cvalues.Logic.logic -> Cvalues.Logic.logic
val map_l2t :
(M.loc -> Lang.F.term) -> Cvalues.Logic.logic -> Cvalues.Logic.logic
val map_t2l :
(Lang.F.term -> M.loc) -> Cvalues.Logic.logic -> Cvalues.Logic.logic
val apply :
Lang.F.binop ->
Cvalues.Logic.logic -> Cvalues.Logic.logic -> Cvalues.Logic.logic
val apply_add :
Cvalues.Logic.logic -> Cvalues.Logic.logic -> Cvalues.Logic.logic
val apply_sub :
Cvalues.Logic.logic -> Cvalues.Logic.logic -> Cvalues.Logic.logic
val field :
Cvalues.Logic.logic -> Cil_types.fieldinfo -> Cvalues.Logic.logic
val shift :
Cvalues.Logic.logic ->
Ctypes.c_object ->
?size:int -> Cvalues.Logic.logic -> Cvalues.Logic.logic
val load :
M.Sigma.t ->
Ctypes.c_object -> Cvalues.Logic.logic -> Cvalues.Logic.logic
val union :
Cil_types.logic_type -> Cvalues.Logic.logic list -> Cvalues.Logic.logic
val inter :
Cil_types.logic_type -> Cvalues.Logic.logic list -> Cvalues.Logic.logic
val subset :
Cil_types.logic_type ->
Cvalues.Logic.logic ->
Cil_types.logic_type -> Cvalues.Logic.logic -> Lang.F.pred
type region = M.loc Memory.sloc list
val separated :
(Ctypes.c_object * Cvalues.Logic.region) list -> Lang.F.pred
val included :
Ctypes.c_object ->
Cvalues.Logic.region ->
Ctypes.c_object -> Cvalues.Logic.region -> Lang.F.pred
val valid :
M.Sigma.t ->
Memory.acs -> Ctypes.c_object -> Cvalues.Logic.region -> Lang.F.pred
end