Up  

Functor MemVar.Make

module Make: 
functor (V : VarUsage) -> 
functor (M : Memory.Model) -> Memory.Model
Parameters:
V : VarUsage
M : Memory.Model 
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 
type state 
val state : sigma -> state
returns a memory state description from a memory model vector.
val lookup : state -> Lang.F.term -> Memory.mval
Try to interpret a term as an in-memory operation located at this program point. Only best-effort shall be performed, otherwise return Mvalue.

Recognized Cil patterns:


val updates : state Memory.sequence -> Lang.F.Vars.t -> Memory.update Bag.t
Try to interpret a sequence of states into updates.

The result shall be exhaustive with respect to values that are printed as Memory.mval values at post label via the lookup function. Otherwise, those values would not be pretty-printed to the user.

val apply : (Lang.F.term -> Lang.F.term) -> state -> state
Propagate a sequent substitution inside the memory state.
val iter : (Memory.mval -> Lang.F.term -> unit) -> state -> unit
Debug
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