functor (M : Memory.Model) ->
sig
type logic = M.loc Memory.logic
type region = M.loc Memory.sloc list
val value : M.loc Memory.logic -> Lang.F.term
val loc : M.loc Memory.logic -> M.loc
val rdescr : M.loc Memory.sloc -> Lang.F.var list * M.loc * Lang.F.pred
val vset_of_sloc : M.loc Memory.sloc list -> Vset.vset list
val sloc_of_vset : Vset.vset list -> M.loc Memory.sloc list
val vset : M.loc Memory.logic -> Vset.set
val sloc : M.loc Memory.logic -> M.loc Memory.sloc list
val is_single : 'a Memory.logic -> bool
val map_lift :
(Lang.F.term -> Lang.F.term) ->
(Vset.set -> Vset.set) -> M.loc Memory.logic -> 'a Memory.logic
val apply_lift :
(Lang.F.term -> Lang.F.term -> Lang.F.term) ->
(Vset.set -> Vset.set -> Vset.set) ->
M.loc Memory.logic -> M.loc Memory.logic -> 'a Memory.logic
val map :
(Lang.F.term -> Lang.F.term) -> M.loc Memory.logic -> 'a Memory.logic
val map_opp : M.loc Memory.logic -> 'a Memory.logic
val apply :
(Lang.F.term -> Lang.F.term -> Lang.F.term) ->
M.loc Memory.logic -> M.loc Memory.logic -> 'a Memory.logic
val apply_add :
M.loc Memory.logic -> M.loc Memory.logic -> 'a Memory.logic
val apply_sub :
M.loc Memory.logic -> M.loc Memory.logic -> 'a Memory.logic
val map_loc : (M.loc -> 'a) -> M.loc Memory.logic -> 'a Memory.logic
val map_l2t :
(M.loc -> Lang.F.term) -> M.loc Memory.logic -> 'a Memory.logic
val map_t2l :
(Lang.F.term -> 'a) -> M.loc Memory.logic -> 'a Memory.logic
val field :
M.loc Memory.logic -> Cil_types.fieldinfo -> M.loc Memory.logic
val restrict : Vset.vset -> int option -> Vset.vset
val shift_set :
M.loc Memory.sloc ->
Ctypes.c_object -> int option -> Vset.vset -> M.loc Memory.sloc
val shift :
M.loc Memory.logic ->
Ctypes.c_object ->
?size:int -> M.loc Memory.logic -> M.loc Memory.logic
type loader = {
mutable sloc : M.loc Memory.sloc list;
mutable vset : Vset.vset list;
}
val flush : bool -> Cvalues.Logic.loader -> M.loc Memory.logic
val loadsloc :
Cvalues.Logic.loader ->
M.sigma -> Ctypes.c_object -> M.loc Memory.sloc -> unit
val load :
M.sigma -> Ctypes.c_object -> M.loc Memory.logic -> M.loc Memory.logic
val union :
Cil_types.logic_type -> M.loc Memory.logic list -> M.loc Memory.logic
val inter :
Cil_types.logic_type -> M.loc Memory.logic list -> 'a Memory.logic
val rloc : Ctypes.c_object -> 'a Memory.sloc -> 'a Memory.rloc
val separated_sloc :
Lang.F.pred list ->
Ctypes.c_object * M.loc Memory.sloc list ->
Ctypes.c_object * M.loc Memory.sloc list -> Lang.F.pred list
val separated_from :
Lang.F.pred list ->
Ctypes.c_object * M.loc Memory.sloc list ->
(Ctypes.c_object * M.loc Memory.sloc list) list -> Lang.F.pred list
val separated_regions :
Lang.F.pred list ->
(Ctypes.c_object * M.loc Memory.sloc list) list -> Lang.F.pred list
val separated :
(Ctypes.c_object * M.loc Memory.sloc list) list -> Lang.F.pred
val included_sloc :
Ctypes.c_object ->
M.loc Memory.sloc ->
Ctypes.c_object -> M.loc Memory.sloc -> Lang.F.pred
val included :
Ctypes.c_object ->
M.loc Memory.sloc list ->
Ctypes.c_object -> M.loc Memory.sloc list -> Lang.F.pred
val valid_sloc :
M.sigma ->
Memory.acs -> Ctypes.c_object -> M.loc Memory.sloc -> Lang.F.pred
val valid :
M.sigma ->
Memory.acs -> Ctypes.c_object -> M.loc Memory.sloc list -> Lang.F.pred
end