Module type Abstract_domain.Transfer

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

type state 
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.
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.
val start_call : Cil_types.stmt ->
value Eval.call ->
valuation ->
state ->
state 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.
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.
val approximate_call : Cil_types.stmt ->
value Eval.call ->
state ->
state list Eval.or_bottom
val show_expr : valuation ->
state -> 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.