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
type
type
type
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.
kinstr is the statement of the assignment, or Kglobal for the
initialization of a global variable.v carries the value being assigned to lv, i.e. the value of the
expression expr. v also denotes the kind of assignment: Assign for
the default assignment of the value, or Copy for the exact copy of a
location if the right expression expr is a lvalue.valuation is a cache of all sub-expressions and locations computed
for the evaluation of lval and expr; it can also be used to reduce
the state.
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.
stmt is the statement of the assumption.valuation is a cache of all sub-expressions and locations computed
for the evaluation and the reduction of expr; it can also be used
to reduce the state
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.
stmt is the statement of the call site;call represents the call: the called function and the arguments;state is the abstract state before the call;valuation is a cache for all values and locations computed during
the evaluation of the function and its arguments.
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.
stmt is the statement of the call site;call represents the function call and its arguments.pre and post are the states before and at the end of the call
respectively.
val approximate_call : Cil_types.stmt ->
value Eval.call ->
state ->
state list Eval.or_bottom