package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

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.

Given an automaton, return a vertex's binder. Currently used by the automata compiler to bind current vertex. See StmtSemantics.

val datatype : string

For projectification. Must be unique among models.

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.

module Sigma : Sigs.Sigma with type chunk = Chunk.t and module Chunk = Heap

Model Environments.

type loc

Representation of the memory location in the model.

type chunk = Chunk.t
type sigma = Sigma.t
type domain = Sigma.domain
type segment = loc Sigs.rloc

Reversing the Model

type state

Internal (private) memory state description for later reversing the model.

val state : sigma -> state

Returns a memory state description from a memory environement.

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 when x has a pointer type
  • Mmem p,[Mfield f;...] is rendered as p->f... like in Cil
  • Mmem p,[Mindex k;...] is rendered as p[k]... to catch Cil Mem(AddPI(p,k)),...

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.

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.

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 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.

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.

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.

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.

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.

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