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 return = return 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 return 
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, return,
value)
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 make_return : Cil_types.kernel_function ->
Cil_types.stmt ->
value Eval.assigned ->
valuation ->
state -> return
make_return kf stmt assigned valuation state makes an abstraction of the return value of the function kf. stmt is the return statement of kf and state the state of the domain at this statement. assigned represents the value of the lvalue being returned, and valuation is the valuation resulting from its evaluation. The return abstraction computed by this function can then be used for the assignment at the call site.
val assign_return : Cil_types.stmt ->
location Eval.left_value ->
Cil_types.kernel_function ->
return ->
value Eval.assigned ->
valuation ->
state ->
state Eval.or_bottom
assign_return stmt lv kf return value valuation state models on states the effect of the assignment of the return value of a called function at the call site.
val default_call : Cil_types.stmt ->
value Eval.call ->
state ->
(state, return,
value)
Eval.call_result
val enter_loop : Cil_types.stmt ->
state -> state
val incr_loop_counter : Cil_types.stmt ->
state -> state
val leave_loop : Cil_types.stmt ->
state -> state