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