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 kf bases state returns the set of bases 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. state is the initial state of an analysis of kf. For a non-relational domain, it is always safe to return empty. For a relational domain, it is always safe to return top, but it disables MemExec.

filter kind bases states reduces the state state to only keep properties about bases — it is a projection on the set of bases. It allows reusing an analysis of kf from an initial state pre to a final state post. If kind is `Pre kf, state is the initial state of function kf, and bases includes all inputs of kf and satisfies relate kf bases state = bases. If kind is `Post kf, state is the final state of kf, and bases includes all inputs and outputs of kf. Afterwards, the two resulting states reduced_pre and reduced_post are used as follow: when kf should be analyzed with the initial state s, if filter kf `Pre s = reduced_pre, then the analysis is skipped, and reuse kf s reduced_post is used as its final state instead. If kind is `Print, the state is reduced before printing it for the end-user.

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

reuse kf bases current_input previous_output merges the initial state current_input with a final state previous_output from a previous analysis of kf started with an equivalent initial state. reuse must overwrite the properties on bases in current_input with the ones in previous_output. Properties on other bases must be left unchanged from current_input.

Domain_builtin.Complete provides the simplest implementation of filter and reuse, which is: let filter _ _ _ state = state let reuse _ _ ~current_input:_ ~previous_output = previous_output This is correct as the cache will be triggered only for an initial state exactly equal to the previous initial state, in which case the previous output state is indeed a correct final state on its own.

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