Module type Memory.Model

module type Model = sig .. end

val configure : Model.tuning
val datatype : string
for projectification
val separation : unit -> Separation.clause list
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 
Representation of the memory location in the model.
type chunk = Memory.Chunk.t 
type sigma = Sigma.t 
type segment = loc Memory.rloc 
val pretty : Format.formatter -> loc -> unit
pretty printing of memory location
val vars : loc -> Lang.F.Vars.t
Return the logic variables from which the given location depend on.
val occurs : Lang.F.var -> loc -> bool
Test if a location depend on a given logic variable
val null : loc
Return the location of the null pointer
val literal : eid:int -> Cstring.cst -> loc
Return the memory location of a constant string, the id is a unique identifier.
val cvar : Cil_types.varinfo -> loc
Return the location of a C variable
val pointer_loc : Lang.F.term -> loc
???
val pointer_val : loc -> Lang.F.term
???
val field : loc -> Cil_types.fieldinfo -> loc
Return the memory location obtained by field access from a given memory location
val shift : loc -> Ctypes.c_object -> Lang.F.term -> loc
Return the memory location obtained by array access at an index represented by the given term. The element of the array are of the given c_object type
val base_addr : loc -> loc
Return the memory location of the base address of a given memory location
val block_length : sigma -> Ctypes.c_object -> loc -> Lang.F.term
Returns the length (in bytes) of the allocated block containing the given location
val cast : Ctypes.c_object Memory.sequence -> loc -> loc
Cast a memory location into another memory location. For cast ty loc the cast is done from ty.pre to ty.post
val loc_of_int : Ctypes.c_object -> Lang.F.term -> loc
Cast a term representing a pointer to a c_object into a memory location
val int_of_loc : Ctypes.c_int -> loc -> Lang.F.term
Cast a memory location into an integer of the given type
val domain : Ctypes.c_object -> loc -> Heap.set
Give the set of chunk where an object of the given type at the given location is stored. Over approximation of this set is allowed.
val load : sigma ->
Ctypes.c_object -> loc -> loc Memory.value
Return the value of the object of the given type at the given location in the given memory state
val copied : sigma Memory.sequence ->
Ctypes.c_object -> loc -> loc -> Lang.F.pred list
Return a set of formula that express a copy between two memory state. copied sigma ty loc1 loc2 returns a set of formula that express that the content for an object ty is the same in sigma.pre at loc1 and in sigma.post at loc2
val stored : sigma Memory.sequence ->
Ctypes.c_object -> loc -> Lang.F.term -> Lang.F.pred list
Return a set of formula that express a modification between two memory state. copied sigma ty loc t returns a set of formula that express that sigma.pre and sigma.post are identical except for an object ty at location loc which is represented by t in sigma.post.
val assigned : sigma Memory.sequence ->
Ctypes.c_object -> loc Memory.sloc -> Lang.F.pred list
Return a set of formula that express that two memory state are the same except at the given set of memory location. This function can over-approximate the set of given memory location (e.g it can return true as if the all set of memory location was given)
val is_null : loc -> Lang.F.pred
Return the formula that check if a given location is null
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
Memory location comparisons
val loc_diff : Ctypes.c_object -> loc -> loc -> Lang.F.term
Compute the length in bytes between two memory locations
val valid : sigma -> Memory.acs -> segment -> Lang.F.pred
Return the formula that tests if a memory state is valid (according to Memory.acs) in the given memory state at the given segment.
val scope : sigma ->
Mcfg.scope -> Cil_types.varinfo list -> sigma * Lang.F.pred list
Manage the scope of variables. Returns the updated memory model and hypotheses modeling the new validity-scope of the variables.
val global : sigma -> Lang.F.term -> Lang.F.pred
Given a pointer value p, assumes this pointer p (when valid) is allocated outside the function frame under analysis. This means separated from the formals and locals of the function.
val included : segment -> segment -> Lang.F.pred
Return the formula that tests if two segment are included
val separated : segment -> segment -> Lang.F.pred
Return the formula that tests if two segment are separated