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