Module type Abstract_domain.Transfer

module type Transfer = sig .. end

Transfer function of the domain.

type state

type return

type value

type location

type valuation

val update : valuation ->
       state -> state

update valuation t updates the state t by the values of expressions and the locations of lvalues stored in valuation.

val assign : Cil_types.kinstr ->
       location Eval.left_value ->
       Cil_types.exp ->
       value Eval.assigned ->
       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.
v carries the value being assigned to lv, i.e. the value of the expression expr. v also denotes the kind of assignement: Assign for the default assignment of the value, or Copy for the exact copy of a location if the right expresssion 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 ->
       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 ->
       value Eval.call ->
       valuation ->
       state ->
       (state, return,
        value)
       Eval.call_action

Decision on a function call: start_call stmt call valuation state decides on the analysis of a call site. It returns either an initial state for a standard dataflow analysis of the called function, or a direct result for the entire call. See Eval.call_action for details.

stmt is the statement of the call site;
call represents the call: the called function and the arguments;
state is the abstract state 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 ->
       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 make_return : Cil_types.kernel_function ->
       Cil_types.stmt ->
       value Eval.assigned ->
       valuation ->
       state -> return

make_return kf stmt assigned valuation state makes an abstraction of the return value of the function kf. stmt is the return statement of kf and state the state of the domain at this statement. assigned represents the value of the lvalue being returned, and valuation is the valuation resulting from its evaluation. The return abstraction computed by this function can then be used for the assignment at the call site.

val assign_return : Cil_types.stmt ->
       location Eval.left_value ->
       Cil_types.kernel_function ->
       return ->
       value Eval.assigned ->
       valuation ->
       state ->
       state Eval.or_bottom

assign_return stmt lv kf return value valuation state models on states the effect of the assignment of the return value of a called function at the call site.

stmt is the statement of the call;
lv is the lvalue being assigned, with its type and location;
kf is the called function, whose return is assigned;
return is an abstraction of this return, computed by make_return;
value is a value abstraction for this return, computed by a standard evaluation in the called function kf;
valuation results from the evaluation of the location of lv;
state is the state before the assignment, but after the call.

val default_call : Cil_types.stmt ->
       value Eval.call ->
       state ->
       (state, return,
        value)
       Eval.call_result

val enter_loop : Cil_types.stmt ->
       state -> state

val incr_loop_counter : Cil_types.stmt ->
       state -> state

val leave_loop : Cil_types.stmt ->
       state -> state