Module type Abstract_domain.Transfer

module type Transfer = sig .. end
Transfer function of the domain.

type state 
type summary 
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 cached in valuation.
val assign : Cil_types.kinstr ->
location Eval.left_value ->
Cil_types.exp ->
value Eval.assigned ->
valuation ->
state ->
state Eval.or_bottom
assign lv expr v valuation state is the transfer function for the assignment lv = expr in state. It must return the state where the assignment has been performed. v is the value corresponding to the already-evaluated expression exp. 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 exp bool valuation state returns a state in which the boolean expression exp evaluates to bool. 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 call_action : Cil_types.stmt ->
value Eval.call ->
valuation ->
state ->
(state, summary,
value)
Eval.action
Decision on a function call: call_action stmt call valuation state decides on the analysis of the called function; see for details on the action type, which described the analysis. stmt is the statement of the call, call represents the call (the called function and the arguments) and state the state before the call.
val summarize : Cil_types.kernel_function ->
Cil_types.stmt ->
returned:(location Eval.left_value *
value Eval.copied)
option ->
state ->
(summary * state)
Eval.or_bottom
summarize kf stmt ~returned_lv state returns a summary of the state state at the end of the function kf. This summary will be used at the call site for the analysis of the calling function. stmt is the return statement of kf, and returned_lv is None if no value is returned, or represents the return lvalue, its type and its location (see for details).
val resolve_call : Cil_types.stmt ->
value Eval.call ->
assigned:(location Eval.left_value *
value Eval.copied)
option ->
valuation ->
pre:state ->
post:summary * state ->
state Eval.or_bottom
resolve_call stmt ~assigned_lv call valuation ~pre_state ~post_state compute the state after the statement stmt where the lvalue assigned is assigned to the result of the call call.
val default_call : Cil_types.stmt ->
value Eval.call ->
state ->
(state, summary,
value)
Eval.call_result