Module LogicSemantics.Make.L

module L: Cvalues.Logic(M)

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 -> loader -> M.loc Memory.logic
val loadsloc : 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