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 ->
Eval.recursion option ->
(value, location,
origin)
Abstract_domain.valuation ->
state ->
state Eval.or_bottom

start_call stmt call recursion 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.

On recursive calls, recursion contains some substitution of variables to be applied on the domain state to prevent mixing up local variables and formal parameters of different recursive calls. See Eval.recursion for more details. This substitution has been applied on values and expressions in call, but not in the valuation given as argument. If the domain uses some information from the valuation on a recursive call, it must apply the substitution on it.

val finalize_call : Cil_types.stmt ->
(location, value) Eval.call ->
Eval.recursion option ->
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_domain_show_each directive. 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. Defined by Domain_builder.Complete but prints nothing.