Frama-C:
Plug-ins:
Libraries:

Frama-C API - Cvalue_queries

Implementation of domain queries for the cvalue domain.

include Abstract_domain.Queries with type state = Frama_c_kernel.Cvalue.Model.t and type context = unit and type value = Main_values.CVal.t and type location = Main_locations.PLoc.location and type origin = Main_values.CVal.t

Domain state.

type context = unit

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 = Main_values.CVal.t

Numerical values to which the expressions are evaluated.

Abstract memory locations associated to left values.

type origin = Main_values.CVal.t

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.

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.

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 : state -> Eval.lval -> location -> value -> (location * value) 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 : state -> Eval.exp -> value -> (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 : state -> context 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.

Evaluation engine specific to the cvalue domain.

include Evaluation_sig.S with type state := state and type context := unit and type value := value and type loc := location and type origin := origin
module Valuation : Eval.Valuation with type value = value and type origin = origin and type loc = location

Results of an evaluation: the results of all intermediate calculation (the value of each expression and the location of each lvalue) are cached here. See Eval for more details.

val to_domain_valuation : Valuation.t -> (value, location, origin) Abstract_domain.valuation

Evaluation functions store the results of an evaluation into Valuation.t maps. Abstract domains read these results from Abstract_domain.valuation records. This function converts the former into the latter.

val evaluate : ?valuation:Valuation.t -> ?reduction:bool -> ?subdivnb:int -> state -> Eval.exp -> (Valuation.t * value) Eval.evaluated

evaluate ~valuation state expr evaluates the expression expr in the state state, and returns the pair result, alarms, where:

  • alarms are the set of alarms ensuring the soundness of the evaluation;
  • result is either `Bottom if the evaluation leads to an error, or `Value (valuation, value), where value is the numeric value computed for the expression expr, and valuation contains all the intermediate results of the evaluation.

Optional arguments are:

  • valuation is a cache of already computed expressions; empty by default.
  • reduction allows the deactivation of the backward reduction performed after the forward evaluation; true by default.
  • subdivnb is the maximum number of subdivisions performed on non-linear sub-expressions of expr. If a lvalue occurs several times in expr, its value can be split up to subdivnb times to gain more precision. Set to the value of the option -eva-subdivide-non-linear by default.
val copy_lvalue : ?valuation:Valuation.t -> ?subdivnb:int -> state -> Eval.lval -> (Valuation.t * value Eval.flagged_value) Eval.evaluated

Computes the value of a lvalue, with possible indeterminateness: the returned value may be uninitialized, or contain escaping addresses. Also returns the alarms resulting of the evaluation of the lvalue location, and a valuation containing all the intermediate results of the evaluation. The valuation argument is a cache of already computed expressions. It is empty by default. subdivnb is the maximum number of subdivisions performed on non-linear expressions.

val lvaluate : ?valuation:Valuation.t -> ?subdivnb:int -> for_writing:bool -> state -> Eval.lval -> (Valuation.t * location) Eval.evaluated

lvaluate ~valuation ~for_writing state lval evaluates the left value lval in the state state. Same general behavior as evaluate above but evaluates the lvalue into a location and its type. The boolean for_writing indicates whether the lvalue is evaluated to be read or written. It is useful for the emission of the alarms, and for the reduction of the location. subdivnb is the maximum number of subdivisions performed on non-linear expressions (including the possible pointer and offset of the lvalue).

val reduce : ?valuation:Valuation.t -> state -> Eval.exp -> bool -> Valuation.t Eval.evaluated

reduce ~valuation state expr positive evaluates the expression expr in the state state, and then reduces the valuation such that the expression expr evaluates to a zero or a non-zero value, according to positive. By default, the empty valuation is used.

val assume : ?valuation:Valuation.t -> state -> Eval.exp -> value -> Valuation.t Eval.or_bottom

assume ~valuation state expr value assumes in the valuation that the expression expr has the value value in the state state, and backward propagates this information to the subterm of expr. If expr has not been already evaluated in the valuation, its forward evaluation takes place first, but the alarms are dismissed. By default, the empty valuation is used. The function returns the updated valuation, or bottom if it discovers a contradiction.

val eval_function : ?subdivnb:int -> Eval.lhost -> ?args:Eval.exp list -> state -> (Frama_c_kernel.Kernel_function.t * Valuation.t) list Eval.or_top_bottom * Alarmset.t

Evaluation of the function argument of a Cil_types.Call constructor. In case of a function pointer, returns:

  • the alarms raised by the evaluation of the pointer, plus an alarm Alarms.Function_pointer if it may not evaluate to a valid function for arguments args (if provided).
  • `Top if the pointer cannot be evaluated (if cvalue is disabled);
  • `Bottom if the pointer evaluates to bottom.
  • or the list of possible functions. Each function f is paired with a valuation obtained by assuming the pointer evaluates exactly to f.
val interpret_truth : alarm:(unit -> Frama_c_kernel.Alarms.t) -> 'a -> 'a Abstract_value.truth -> 'a Eval.evaluated

Evaluates the location of a lvalue in a given cvalue state.