Module type Memory.Model

module type Model = sig .. end

val configure : Model.tuning
val datatype : string
for projectification
module Chunk: Memory.Chunk 
module Heap: Qed.Collection.S  
    with type t = Chunk.t
module Sigma: Memory.Sigma 
    with type chunk = Chunk.t
    and type domain = Heap.set
type loc 
type chunk = Memory.Chunk.t 
type sigma = Sigma.t 
type segment = loc Memory.rloc 
val pretty : Format.formatter -> loc -> unit
val vars : loc -> Lang.F.Vars.t
val occurs : Lang.F.var -> loc -> bool
val null : loc
val literal : eid:int -> Cstring.cst -> loc
val cvar : Cil_types.varinfo -> loc
val pointer_loc : Lang.F.term -> loc
val pointer_val : loc -> Lang.F.term
val field : loc -> Cil_types.fieldinfo -> loc
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 domain : Ctypes.c_object -> loc -> Heap.set
val load : sigma ->
Ctypes.c_object -> loc -> loc Memory.value
val copied : sigma Memory.sequence ->
Ctypes.c_object -> loc -> loc -> Lang.F.pred list
val stored : sigma Memory.sequence ->
Ctypes.c_object -> loc -> Lang.F.term -> Lang.F.pred list
val assigned : sigma Memory.sequence ->
Ctypes.c_object -> loc Memory.sloc -> Lang.F.pred list
val is_null : loc -> Lang.F.pred
val loc_eq : loc -> loc -> Lang.F.pred
val loc_lt : loc -> loc -> Lang.F.pred
val loc_neq : loc -> loc -> Lang.F.pred
val loc_leq : loc -> loc -> Lang.F.pred
val loc_diff : Ctypes.c_object -> loc -> loc -> Lang.F.term
val valid : sigma -> Memory.acs -> segment -> Lang.F.pred
val scope : sigma ->
Mcfg.scope -> Cil_types.varinfo list -> sigma * Lang.F.pred list
val included : segment -> segment -> Lang.F.pred
val separated : segment -> segment -> Lang.F.pred