Frama-C:
Plug-ins:
Libraries:

Frama-C API - Dom

type state
include Frama_c_kernel.Datatype.S_with_collections with type t = state
include Frama_c_kernel.Datatype.S with type t = state
include Frama_c_kernel.Datatype.S_no_copy with type t = state
include Frama_c_kernel.Datatype.Ty with type t = state
type t = state

Datatype descriptor.

Packed version of the descriptor.

val reprs : t list

List of representants of the descriptor.

val equal : t -> t -> bool

Equality: same spec than Stdlib.(=).

val compare : t -> t -> int

Comparison: same spec than Stdlib.compare.

val hash : t -> int

Hash function: same spec than Hashtbl.hash.

val pretty : Stdlib.Format.formatter -> t -> unit

Pretty print each value in an user-friendly way.

val mem_project : (Frama_c_kernel.Project_skeleton.t -> bool) -> t -> bool

mem_project f x must return true iff there is a value p of type Project.t in x such that f p returns true.

val copy : t -> t

Deep copy: no possible sharing between x and copy x.

module Set : Frama_c_kernel.Datatype.Set with type elt = t
module Map : Frama_c_kernel.Datatype.Map with type key = t
val name : string

Lattice Structure

val top : t

Greatest element.

val is_included : t -> t -> bool

Inclusion test.

val join : t -> t -> t

Semi-lattice structure.

widen h t1 t2 is an over-approximation of join t1 t2. Assumes is_included t1 t2

val narrow : t -> t -> t Eva.Eval.or_bottom

Over-approximation of the intersection of two abstract states (called meet in the literature). Used only to gain some precision when interpreting the complete behaviors of a function specification. Can be very imprecise without impeding the analysis: meet x y = `Value x is always sound.

Queries

type context = Ctx.t

Domains can optionally provide a context to be used by value abstractions when evaluating expressions. This can be safely ignored for most domains. Defined as unit (no context) by Domain_builder.Complete.

type value = Val.t

Numerical values to which the expressions are evaluated.

type location = Loc.location

Abstract memory locations associated to left values.

type origin

The origin is used by the domain combiners to track the origin of a value. An abstract domain can always use a dummy type unit for origin, or use it to encode some specific information about a value.

Queries functions return a pair of:

  • the set of alarms that ensures the of the soundness of the evaluation of exp. Alarmset.all is always a sound over-approximation of these alarms.
  • a value for the expression, which can be: – `Bottom if its evaluation is infeasible; – `Value (v, o) where v is an over-approximation of the abstract value of the expression exp, and o is the origin of the value, which can be None.

When evaluating an expression, the evaluation engine asks the domains for abstract values and alarms at each lvalue (via extract_lval) and each sub-expressions (via extract_expr). In these queries:

  • oracle is an evaluation function and can be used to find the answer by evaluating some others expressions, especially by relational domain. No recursive evaluation should be done by this function.
  • context record gives some information about the current evaluation.
val extract_expr : oracle:(Eva.Eval.exp -> value Eva.Eval.evaluated) -> Eva__.Abstract_domain.evaluation_context -> t -> Eva.Eval.exp -> (value * origin option) Eva.Eval.evaluated

Query function for compound expressions: extract_expr ~oracle context t exp returns the known value of exp by the state t. See above for more details on queries.

val extract_lval : oracle:(Eva.Eval.exp -> value Eva.Eval.evaluated) -> Eva__.Abstract_domain.evaluation_context -> t -> Eva.Eval.lval -> location -> (value * origin option) Eva.Eval.evaluated

Query function for lvalues: extract_lval ~oracle context t lval loc returns the known value stored at the location loc of the left value lval. See above for more details on queries.

val backward_location : t -> Eva.Eval.lval -> location -> value -> (location * value) Eva.Eval.or_bottom

backward_location state lval typ loc v reduces the location loc of the lvalue lval, so that only the locations that may have value v are kept. The returned location must be included in loc, but it is always sound to return loc itself. Also returns the value that may have the returned location, if not bottom. Defined by Domain_builder.Complete with no reduction.

val reduce_further : t -> Eva.Eval.exp -> value -> (Eva.Eval.exp * value) list

Given a reduction expr = value, provides more reductions that may be performed. Defined by Domain_builder.Complete with no reduction.

val build_context : t -> context Eva.Eval.or_bottom

Returns the current context to be used by value abstractions for the evaluation of expressions or lvalues. Defined by Domain_builder.Complete with no context.

Transfer Functions

Transfer functions from the result of evaluations. See Eval for more details about valuation.

val update : (value, location, origin) Eva__.Abstract_domain.valuation -> t -> t Eva.Eval.or_bottom

update valuation t updates the state t with the values of expressions and the locations of lvalues available in the valuation record.

assign kinstr lv expr v valuation state is the transfer function for the assignment lv = expr for state. It must return the state where the assignment has been performed.

  • kinstr is the statement of the assignment, or Kglobal for the initialization of a global variable.
  • when the kinstr is a function call, expr is the special variable in !Eval.call.return.
  • v carries the value being assigned to lv, i.e. the value of the expression expr. v also denotes the kind of assignment: Assign for the default assignment of the value, or Copy for the exact copy of a location if the right expression expr is a lvalue.
  • valuation is a cache of all sub-expressions and locations computed for the evaluation of lval and expr; it can also be used to reduce the state.
val assume : Frama_c_kernel.Cil_types.stmt -> Eva.Eval.exp -> bool -> (value, location, origin) Eva__.Abstract_domain.valuation -> t -> t Eva.Eval.or_bottom

Transfer function for an assumption. assume stmt expr bool valuation state returns a state in which the boolean expression expr evaluates to bool.

  • stmt is the statement of the assumption.
  • valuation is a cache of all sub-expressions and locations computed for the evaluation and the reduction of expr; it can also be used to reduce the state.
val start_call : Frama_c_kernel.Cil_types.stmt -> (location, value) Eva.Eval.call -> Eva.Eval.recursion option -> (value, location, origin) Eva__.Abstract_domain.valuation -> t -> t Eva.Eval.or_bottom

start_call stmt call recursion valuation state returns an initial state for the analysis of a called function. In particular, this function should introduce the formal parameters in the state, if necessary.

  • stmt is the statement of the call site;
  • call represents the call: the called function and the arguments;
  • recursion is the information needed to interpret a recursive call. It is None if the call is not recursive.
  • state is the abstract state at the call site, before the call;
  • valuation is a cache for all values and locations computed during the evaluation of the function and its arguments.

On recursive calls, recursion contains some substitution of variables to be applied on the domain state to prevent mixing up local variables and formal parameters of different recursive calls. See Eval.recursion for more details. This substitution has been applied on values and expressions in call, but not in the valuation given as argument. If the domain uses some information from the valuation on a recursive call, it must apply the substitution on it.

finalize_call stmt call ~pre ~post computes the state after a function call, given the state pre before the call, and the state post at the end of the called function.

  • stmt is the statement of the call site;
  • call represents the function call and its arguments.
  • recursion is the information needed to interpret a recursive call. It is None if the call is not recursive.
  • pre and post are the states before and at the end of the call respectively.
val show_expr : (value, location, origin) Eva__.Abstract_domain.valuation -> t -> Stdlib.Format.formatter -> Eva.Eval.exp -> unit

Called on the Frama_C_domain_show_each directive. Prints the internal properties inferred by the domain in the state about the expression exp. Can use the valuation resulting from the cooperative evaluation of the expression. Defined by Domain_builder.Complete but prints nothing.

Logic

Logical evaluation. This API is subject to changes.

val logic_assign : (location Eva.Eval.logic_assign * state) option -> location -> state -> state

logic_assign None loc state removes from state all inferred properties that depend on the memory location loc. If the first argument is not None, it contains the logical clause being interpreted and the pre-state in which the terms of the clause are evaluated. The clause can be an assigns, allocates or frees clause. loc is then the memory location concerned by the clause.

val evaluate_predicate : state Eva__.Abstract_domain.logic_environment -> state -> Frama_c_kernel.Cil_types.predicate -> Frama_c_kernel.Abstract_interp.Comp.result

Evaluates a predicate to a logical status in the current state. The logic_environment contains the states at some labels and the potential variable for \result. Defined by Domain_builder.Complete: all predicates are Unknown.

val reduce_by_predicate : state Eva__.Abstract_domain.logic_environment -> state -> Frama_c_kernel.Cil_types.predicate -> bool -> state Eva.Eval.or_bottom

reduce_by_predicate env state pred b reduces the current state by assuming that the predicate pred evaluates to b. env contains the states at some labels and the potential variable for \result. Defined by Domain_builder.Complete with no reduction.

val interpret_acsl_extension : Frama_c_kernel.Cil_types.acsl_extension -> state Eva__.Abstract_domain.logic_environment -> state -> state

Interprets an ACSL extension. Defined by Domain_builder.Complete as the identity.

Scoping and initialization

Scoping: abstract transformers for entering and exiting blocks. The variables should be added or removed from the abstract state here. Note that the formals of a called function enter the scope through the transfer function start_call, and leave it through a call to leave_scope.

val enter_scope : Eva__.Abstract_domain.variable_kind -> Frama_c_kernel.Cil_types.varinfo list -> t -> t

Introduces a list of variables in the state. At this point, the variables are uninitialized. Globals and formals of the 'main' will be initialized by initialize_variable and initialize_variable_using_type. Local variables remain uninitialized until an assignment through assign. The formal parameters of a call enter the scope through start_call.

Removes a list of local and formal variables from the state. The first argument is the englobing function.

val empty : unit -> t

The initial state with which the analysis start.

val initialize_variable : Eva.Eval.lval -> location -> initialized:bool -> Eva__.Abstract_domain.init_value -> t -> t

initialize_variable lval loc ~initialized init_value state initializes the value of the location loc of lvalue lval in state with: – bits 0 if init_value = Zero; – any bits if init_value = Top. The boolean initialized is true if the location is initialized, and false if the location may be not initialized.

val initialize_variable_using_type : Eva__.Abstract_domain.variable_kind -> Frama_c_kernel.Cil_types.varinfo -> t -> t

Initializes a variable according to its type. The variable can be:

  • a global variable on lib-entry mode.
  • a formal parameter of the 'main' function.
  • the return variable of a function specification.

Miscellaneous

Transfer functions called when entering/leaving a loop, and at each loop iteration. Defined as identity by Domain_builder.Complete.

val incr_loop_counter : Frama_c_kernel.Cil_types.stmt -> state -> state

relate bases state returns the set of bases in relation with bases in state — i.e. all bases (other than bases) whose value may affect the properties inferred on bases in state. For a non-relational domain, it is always sound to return empty. For a relational domain, it is always sound to return top, but this disables the MemExec cache.

val filter : Frama_c_kernel.Base.Hptset.t -> t -> t

filter bases state returns a state that must contain exactly the same properties about bases as state. All properties about other bases can be removed from the state. If S' = filter B S, S' must satisfy proj(γ(S'), B) = proj(γ(S), B). Defined by Domain_builder.Complete as the identity, which is sound but decreases the performance of the MemExec cache. If you implement filter, you must also provide a sound implementation of reuse.

val reuse : Frama_c_kernel.Base.Hptset.t -> current_input:t -> previous_output:t -> t

reuse bases ~current_input ~previous_output returns a state equal to current_input, except that all properties about bases must be replaced by the ones in previous_output. It must be exact to ensure that the MemExec cache does not impact the analysis precision. reuse is only applied to re-interpret a code <C> already analyzed with an equivalent initial state. current_input is the new input state for the analysis of <C>, and previous_output was the final state of the former analysis of <C>. See below for details. Defined by Domain_builder.Complete with a naive implementation which is only sound when filter is implemented as the identity.

val project : Frama_c_kernel.Base.Hptset.t -> t -> t

project bases state returns an over-approximation of the projection of state on bases. If S' = project B S, S' must satisfy proj(γ(S), B) ⊆ γ(S'). Defined by Domain_builder.Complete by always returning top.

val overwrite : Frama_c_kernel.Base.Hptset.t -> on:t -> by:t -> t

overwrite bases ~on ~by returns a state equal to on, except that all properties about bases are replaced by the ones in by. Unlike reuse, overwrite can compute an over-approximation, but cannot use any assumption about state on. State by is the result of a projection on bases bases. A sound but imprecise implementation can remove all properties about bases from state on (and ignore state by). More formally, this function must compute an over-approximation of proj(γ(on), complement(bases)) ∩ proj(γ(by), bases), where complement(bases) are all memory bases other than bases.

About the MemExec cache: Assuming a former analysis of function F has computed F(S1) = S1' by reading only bases R and writing only bases W (S1 is the initial state, S1' the final state). For a new initial state S2, if filter R S1 = filter R S2 (the new entry state is exactly the same as the previous one on all read bases), then the analysis S2' = F(S2) is skipped and the final state is computed as S2' = reuse W S2 (filter W S1').

The implementation of reuse can use these assumptions on the set of written bases W, the new initial state S2 and the former final state S1' to compute its result S2'.

val log_category : Eva__.Self.category

Category for the messages about the domain. Created by Domain_builder.Complete using the domain name.

val post_analysis : t Eva.Eval.or_bottom -> unit

This function is called after the analysis. The argument is the state computed at the return statement of the main function. The function can also access all states stored in the Store module during the analysis. If the analysis aborted, this function is not called. Defined by Domain_builder.Complete as doing nothing.

module Store : sig ... end

Storage of the states computed by the analysis. Automatically built by Domain_builder.Complete.

val structure : t Eva__.Abstract.Domain.structure
val mem : 'a Eva__.Structure.Key_Domain.key -> bool

Tests whether a key belongs to the module.

val get : 'a Eva__.Structure.Key_Domain.key -> (t -> 'a) option

For a key of type k key:

  • if the values of type t contain a subpart of type k from a module identified by the key, then get key returns an accessor for it.
  • otherwise, get key returns None.
val set : 'a Eva__.Structure.Key_Domain.key -> 'a -> t -> t

For a key of type k key:

  • if the values of type t contain a subpart of type k from a module identified by the key, then set key v t returns the value t in which this subpart has been replaced by v.
  • otherwise, set key _ is the identity function.

Iterators on the components of a structure.

type polymorphic_iter_fun = {
  1. iter : 'a. 'a Eva__.Structure.Key_Domain.key -> (module Eva__.Abstract_domain.S with type state = 'a) -> 'a -> unit;
}
val iter : polymorphic_iter_fun -> t -> unit
type 'b polymorphic_fold_fun = {
  1. fold : 'a. 'a Eva__.Structure.Key_Domain.key -> (module Eva__.Abstract_domain.S with type state = 'a) -> 'a -> 'b -> 'b;
}
val fold : 'b polymorphic_fold_fun -> t -> 'b -> 'b
type polymorphic_map_fun = {
  1. map : 'a. 'a Eva__.Structure.Key_Domain.key -> (module Eva__.Abstract_domain.S with type state = 'a) -> 'a -> 'a;
}
val map : polymorphic_map_fun -> t -> t