Module type Wp.Memory.Model

module type Model = sig .. end

val configure : Wp.Model.tuning
val datatype : string
for projectification
val separation : unit -> Wp.Separation.clause list
module Chunk: Wp.Memory.Chunk 
module Heap: Qed.Collection.S 
    with type t = Chunk.t
module Sigma: Wp.Memory.Sigma 
    with type chunk = Chunk.t
     and type domain = Heap.set
type loc 
Representation of the memory location in the model.
type chunk = Wp.Memory.Chunk.t 
type sigma = Sigma.t 
type segment = loc Wp.Memory.rloc 
val pretty : Format.formatter -> loc -> unit
pretty printing of memory location
val vars : loc -> Wp.Lang.F.Vars.t
Return the logic variables from which the given location depend on.
val occurs : Wp.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 -> Wp.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 : Wp.Lang.F.term -> loc
???
val pointer_val : loc -> Wp.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 ->
Wp.Ctypes.c_object -> Wp.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 ->
Wp.Ctypes.c_object -> loc -> Wp.Lang.F.term
Returns the length (in bytes) of the allocated block containing the given location
val cast : Wp.Ctypes.c_object Wp.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 : Wp.Ctypes.c_object -> Wp.Lang.F.term -> loc
Cast a term representing a pointer to a c_object into a memory location
val int_of_loc : Wp.Ctypes.c_int -> loc -> Wp.Lang.F.term
Cast a memory location into an integer of the given type
val domain : Wp.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 ->
Wp.Ctypes.c_object ->
loc -> loc Wp.Memory.value
Return the value of the object of the given type at the given location in the given memory state
val copied : sigma Wp.Memory.sequence ->
Wp.Ctypes.c_object ->
loc -> loc -> Wp.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 Wp.Memory.sequence ->
Wp.Ctypes.c_object ->
loc -> Wp.Lang.F.term -> Wp.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 Wp.Memory.sequence ->
Wp.Ctypes.c_object ->
loc Wp.Memory.sloc -> Wp.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 -> Wp.Lang.F.pred
Return the formula that check if a given location is null
val loc_eq : loc -> loc -> Wp.Lang.F.pred
val loc_lt : loc -> loc -> Wp.Lang.F.pred
val loc_neq : loc -> loc -> Wp.Lang.F.pred
val loc_leq : loc -> loc -> Wp.Lang.F.pred
Memory location comparisons
val loc_diff : Wp.Ctypes.c_object ->
loc -> loc -> Wp.Lang.F.term
Compute the length in bytes between two memory locations
val valid : sigma ->
Wp.Memory.acs -> segment -> Wp.Lang.F.pred
Return the formula that tests if a memory state is valid (according to Wp.Memory.acs) in the given memory state at the given segment.
val scope : sigma ->
Wp.Mcfg.scope ->
Cil_types.varinfo list -> sigma * Wp.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 -> Wp.Lang.F.term -> Wp.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 -> Wp.Lang.F.pred
Return the formula that tests if two segment are included
val separated : segment -> segment -> Wp.Lang.F.pred
Return the formula that tests if two segment are separated