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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
val get : 'aEva__.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 : 'aEva__.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 = {
iter : 'a. 'aEva__.Structure.Key_Domain.key->(moduleEva__.Abstract_domain.Swithtypestate = 'a)->'a->
unit;