Module type Abstract_domain.Transfer

module type Transfer = sig .. end

Transfer function of the domain.

type state

type value

type location

type origin

val update : (value, location,
        origin)
       Abstract_domain.valuation ->
       state ->
       state 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.

val assign : Cil_types.kinstr ->
       location Eval.left_value ->
       Cil_types.exp ->
       (location, value)
       Eval.assigned ->
       (value, location,
        origin)
       Abstract_domain.valuation ->
       state ->
       state Eval.or_bottom

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 : Cil_types.stmt ->
       Cil_types.exp ->
       bool ->
       (value, location,
        origin)
       Abstract_domain.valuation ->
       state ->
       state 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 : Cil_types.stmt ->
       (location, value) Eval.call ->
       (value, location,
        origin)
       Abstract_domain.valuation ->
       state ->
       state Eval.or_bottom

start_call stmt call 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;
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.

val finalize_call : Cil_types.stmt ->
       (location, value) Eval.call ->
       pre:state ->
       post:state ->
       state Eval.or_bottom

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.
pre and post are the states before and at the end of the call respectively.

val show_expr : (value, location,
        origin)
       Abstract_domain.valuation ->
       state ->
       Stdlib.Format.formatter -> Cil_types.exp -> unit

Called on the Frama_C_show_each directives. 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.