Frama-C API - M
Model Definition
val configure : unit -> WpContext.rollback
Initializers to be run before using the model. Typically push Context
values and returns a function to rollback.
val configure_ia : Frama_c_kernel.Interpreted_automata.automaton -> Frama_c_kernel.Interpreted_automata.vertex Sigs.binder
Given an automaton, return a vertex's binder. Currently used by the automata compiler to bind current vertex. See StmtSemantics
.
val hypotheses : MemoryContext.partition -> MemoryContext.partition
Computes the memory model partitionning of the memory locations. This function typically adds new elements to the partition received in input (that can be empty).
module Chunk : Sigs.Chunk
Memory model chunks.
module Heap : Qed.Collection.S with type t = Chunk.t
Chunks Sets and Maps.
type chunk = Chunk.t
type sigma = Sigma.t
type domain = Sigma.domain
Reversing the Model
val lookup : state -> Lang.F.term -> Sigs.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:
Mvar x,[Mindex 0]
is rendered as*x
whenx
has a pointer typeMmem p,[Mfield f;...]
is rendered asp->f...
like in CilMmem p,[Mindex k;...]
is rendered asp[k]...
to catch CilMem(AddPI(p,k)),...
val updates : state Sigs.sequence -> Lang.F.Vars.t -> Sigs.update Frama_c_kernel.Bag.t
Try to interpret a sequence of states into updates.
The result shall be exhaustive with respect to values that are printed as Sigs.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 : (Sigs.mval -> Lang.F.term -> unit) -> state -> unit
Debug
val pretty : Stdlib.Format.formatter -> loc -> unit
pretty printing of memory location
Memory Model API
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 : Frama_c_kernel.Cil_types.varinfo -> loc
Return the location of a C variable.
val pointer_loc : Lang.F.term -> loc
Interpret an address value (a pointer) as an abstract location. Might fail on memory models not supporting pointers.
val pointer_val : loc -> Lang.F.term
Return the adress value (a pointer) of an abstract location. Might fail on memory models not capable of representing pointers.
val field : loc -> Frama_c_kernel.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.
Return the memory location of the base address of a given memory location.
val base_offset : loc -> Lang.F.term
Return the offset of the location, in bytes, from its base_addr.
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 Sigs.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
. Might fail on memory models not supporting pointer casts.
val loc_of_int : Ctypes.c_object -> Lang.F.term -> loc
Cast a term representing an absolute memory address (to some c_object) given as an integer, into an abstract memory location.
val int_of_loc : Ctypes.c_int -> loc -> Lang.F.term
Cast a memory location into its absolute memory address, given as an integer with the given C-type.
val domain : Ctypes.c_object -> loc -> domain
Compute the set of chunks that hold the value of an object with the given C-type. It is safe to retun an over-approximation of the chunks involved.
val is_well_formed : sigma -> Lang.F.pred
Provides the constraint corresponding to the kind of data stored by all chunks in sigma.
val load : sigma -> Ctypes.c_object -> loc -> loc Sigs.value
Return the value of the object of the given type at the given location in the given memory state.
val load_init : sigma -> Ctypes.c_object -> loc -> Lang.F.term
Return the initialization status at the given location in the given memory state.
val copied : sigma Sigs.sequence -> Ctypes.c_object -> loc -> loc -> Sigs.equation list
Return a set of equations that express a copy between two memory state.
copied sigma ty loc1 loc2
returns a set of formula expressing that the content for an object ty
is the same in sigma.pre
at loc1
and in sigma.post
at loc2
.
val copied_init : sigma Sigs.sequence -> Ctypes.c_object -> loc -> loc -> Sigs.equation list
Return a set of equations that express a copy of an initialized state between two memory state.
copied sigma ty loc1 loc2
returns a set of formula expressing that the initialization status for an object ty
is the same in sigma.pre
at loc1
and in sigma.post
at loc2
.
val stored : sigma Sigs.sequence -> Ctypes.c_object -> loc -> Lang.F.term -> Sigs.equation list
Return a set of formula that express a modification between two memory state.
stored sigma ty loc t
returns a set of formula expressing 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 stored_init : sigma Sigs.sequence -> Ctypes.c_object -> loc -> Lang.F.term -> Sigs.equation list
Return a set of formula that express a modification of the initialization status between two memory state.
stored_init sigma ty loc t
returns a set of formula expressing that sigma.pre
and sigma.post
are identical except for an object ty
at location loc
which has a new init represented by t
in sigma.post
.
val assigned : sigma Sigs.sequence -> Ctypes.c_object -> loc Sigs.sloc -> Sigs.equation 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 -> Sigs.acs -> segment -> Lang.F.pred
Return the formula that tests if a memory state is valid (according to acs
) in the given memory state at the given segment.
val frame : sigma -> Lang.F.pred list
Assert the memory is a proper heap state preceeding the function entry point.
val alloc : sigma -> Frama_c_kernel.Cil_types.varinfo list -> sigma
Allocates new chunk for the validity of variables.
val initialized : sigma -> segment -> Lang.F.pred
Return the formula that tests if a memory state is initialized (according to acs
) in the given memory state at the given segment.
val invalid : sigma -> segment -> Lang.F.pred
Returns the formula that tests if the entire memory is invalid for write access.
val scope : sigma Sigs.sequence -> Sigs.scope -> Frama_c_kernel.Cil_types.varinfo list -> 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