Frama-C API - Transfer

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

assign ~pos 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.

• pos is the position of the assignment, designating either a global initialization or a function assignment statement with the current callstack.
• when the position 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 ~pos expr bool valuation state returns a state in which the boolean expression expr evaluates to bool.

• pos is the analysis position 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 ~pos 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.

• pos is the analysis position 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 ~pos call recursion ~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.

• pos is the analysis position 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.