Functor MemVar.Make

module Make: 
functor (V : VarUsage) ->
functor (M : Memory.Model) -> sig .. end
Parameters:
V : VarUsage
M : Memory.Model

val datatype : string
val configure : Model.tuning
type chunk = 
| Var of Cil_types.varinfo
| Alloc of Cil_types.varinfo
| Mem of M.Chunk.t
val is_framed_var : Cil_types.varinfo -> bool
module VAR: sig .. end
module VALLOC: sig .. end
module Chunk: sig .. end
module HEAP: Qed.Collection.Make(VAR)
module TALLOC: Qed.Collection.Make(VALLOC)
module SIGMA: Sigma.Make(VAR)(HEAP)
module ALLOC: Sigma.Make(VALLOC)(TALLOC)
module Heap: Qed.Collection.Make(Chunk)
type sigma = {
   mem : M.Sigma.t;
   vars : SIGMA.t;
   alloc : ALLOC.t;
}
module Sigma: sig .. end
val get_var : sigma -> SIGMA.chunk -> Lang.F.var
val get_term : sigma -> SIGMA.chunk -> Lang.F.term
type loc = 
| Mloc of M.loc
| Fref of Cil_types.varinfo
| Fval of Cil_types.varinfo * ofs list
| Mval of Cil_types.varinfo * ofs list
type ofs = 
| Field of Cil_types.fieldinfo
| Index of Ctypes.c_object * Lang.F.term
type segment = loc Memory.rloc 
val pp_ofs : Format.formatter -> ofs list -> unit
val pretty : Format.formatter -> loc -> unit
val ofs_vars : Lang.F.Vars.t -> ofs list -> Lang.F.Vars.t
val vars : loc -> Lang.F.Vars.t
val ofs_occurs : Lang.F.Vars.elt -> ofs list -> bool
val occurs : Lang.F.var -> loc -> bool
val null : loc
val literal : eid:int -> Cstring.cst -> loc
val cvar : Cil_types.varinfo -> loc
val mloc : Cil_types.varinfo -> ofs list -> M.loc
val mloc_of_loc : loc -> M.loc
val pointer_loc : Lang.F.term -> loc
val pointer_val : loc -> Lang.F.term
val field : loc -> Cil_types.fieldinfo -> loc
val index : ofs list ->
Ctypes.c_object -> Lang.F.term -> ofs list
val shift : loc -> Ctypes.c_object -> Lang.F.term -> loc
val base_addr : loc -> loc
val block_length : sigma -> Ctypes.c_object -> loc -> Lang.F.term
val cast : Ctypes.c_object Memory.sequence -> loc -> loc
val loc_of_int : Ctypes.c_object -> Lang.F.term -> loc
val int_of_loc : Ctypes.c_int -> loc -> Lang.F.term
val access : Lang.F.term -> ofs list -> Lang.F.term
val update : Lang.F.term -> ofs list -> Lang.F.term -> Lang.F.term
val mload : sigma -> Ctypes.c_object -> M.loc -> loc Memory.value
val load : sigma ->
Ctypes.c_object -> loc -> loc Memory.value
val mstored : sigma Memory.sequence ->
Ctypes.c_object -> M.loc -> Lang.F.term -> Lang.F.pred list
val stored : sigma Memory.sequence ->
Ctypes.c_object -> loc -> Lang.F.term -> Lang.F.pred list
val copied : sigma Memory.sequence ->
Ctypes.c_object -> loc -> loc -> Lang.F.pred list
val is_null : loc -> Lang.F.pred
val offset : ofs list -> Lang.F.term
val loc_diff : Ctypes.c_object -> loc -> loc -> Lang.F.term
val loc_compare : (M.loc -> M.loc -> Lang.F.pred) ->
(Lang.F.term -> Lang.F.term -> Lang.F.pred) ->
Lang.F.pred -> loc -> loc -> Lang.F.pred
val loc_eq : loc -> loc -> Lang.F.pred
val loc_lt : loc -> loc -> Lang.F.pred
val loc_leq : loc -> loc -> Lang.F.pred
val loc_neq : loc -> loc -> Lang.F.pred
val size_of_array_type : Cil_types.typ -> Lang.F.term option
val first_index : Lang.F.term option
val range_offset : Cil_types.typ -> Lang.F.term -> Lang.F.pred
val valid_offset : Cil_types.typ -> ofs list -> Lang.F.pred
val valid_offsetrange : Cil_types.typ ->
ofs list ->
Lang.F.term option -> Lang.F.term option -> Lang.F.pred
val valid_base : sigma -> Memory.acs -> ALLOC.chunk -> Lang.F.pred
val valid_path : sigma ->
Memory.acs ->
ALLOC.chunk ->
Cil_types.typ -> ofs list -> Lang.F.pred
val valid_pathrange : sigma ->
Memory.acs ->
ALLOC.chunk ->
Cil_types.typ ->
ofs list ->
Lang.F.term option -> Lang.F.term option -> Lang.F.pred
val valid_loc : sigma ->
Memory.acs -> Ctypes.c_object -> loc -> Lang.F.pred
val valid_range : sigma ->
Memory.acs ->
loc ->
Ctypes.c_object -> Lang.F.term option -> Lang.F.term option -> Lang.F.pred
val valid_array : sigma ->
Memory.acs -> loc -> Ctypes.c_object -> int -> Lang.F.pred
val valid : sigma -> Memory.acs -> loc Memory.rloc -> Lang.F.pred
val is_mem : Cil_types.varinfo -> bool
val is_ref : Cil_types.varinfo -> bool
val alloc_var : ALLOC.t ->
TALLOC.Set.t -> Lang.F.term -> Lang.F.pred list
val allocates : ALLOC.t ->
TALLOC.Set.elt list ->
bool -> ALLOC.t * Lang.F.pred list
val framed : sigma -> Lang.F.pred list
val scope_vars : sigma ->
Mcfg.scope ->
TALLOC.Set.elt list -> ALLOC.t * Lang.F.pred list
val scope : sigma ->
Mcfg.scope ->
TALLOC.Set.elt list -> sigma * Lang.F.pred list
val global : sigma -> Lang.F.term -> Lang.F.pred
type seq = 
| Rseg of Cil_types.varinfo
| Fseg of Cil_types.varinfo * delta list
| Mseg of M.loc Memory.rloc * Cil_types.varinfo * delta list
| Lseg of M.loc Memory.rloc
type delta = 
| Dfield of Cil_types.fieldinfo
| Drange of Lang.F.term option * Lang.F.term option
val dofs : ofs -> delta
val delta : ofs list -> delta list
val range : ofs list ->
Ctypes.c_object ->
Lang.F.term option -> Lang.F.term option -> delta list
val dsize : int -> delta
val rsize : ofs list -> int -> delta list
val locseg : loc Memory.rloc -> seq
val included_delta : delta list -> delta list -> Lang.F.pred
val included : loc Memory.rloc -> loc Memory.rloc -> Lang.F.pred
val separated_delta : delta list -> delta list -> Lang.F.pred
val separated : loc Memory.rloc -> loc Memory.rloc -> Lang.F.pred
val sloc_descr : loc Memory.sloc ->
Lang.F.var list * loc * Lang.F.pred
val floc_path : loc -> Cil_types.varinfo * ofs list
val assigned_path : Lang.F.pred list ->
Lang.F.var list ->
Lang.F.var list ->
Lang.F.term -> Lang.F.term -> ofs list -> Lang.F.pred list
val assigned : sigma Memory.sequence ->
Ctypes.c_object -> loc Memory.sloc -> Lang.F.pred list
val domain : Ctypes.c_object -> loc -> Heap.Set.t