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 ->
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.