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