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