Functor Abstract_domain.S.Transfer

module Transfer: 
functor (Valuation : Abstract_domain.Valuation with type value = value and type origin = origin and type loc = location-> Abstract_domain.Transfer with type state := t and type value := value and type location := location and type valuation := Valuation.t

Transfer functions from the result of evaluations. See for more details about valuation.

Parameters:
Valuation : Valuation with type value = value and type origin = origin and type loc = location

type state 
type value 
type location 
type valuation 
val update : valuation ->
state ->
state Eval.or_bottom

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 ->
(location, 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 ->
(location, value) Eval.call ->
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 : 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.