module type Transfer =sig..end
Transfer function of the domain.
type
type
type
type
val update : (value, location,
origin)
Abstract_domain.valuation ->
state ->
state Eval.or_bottomupdate 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_bottomassign 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.expr is the special variable in
!Eval.call.return.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 ->
(value, location,
origin)
Abstract_domain.valuation ->
state ->
state Eval.or_bottomTransfer 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 ->
(location, value) Eval.call ->
Eval.recursion option ->
(value, location,
origin)
Abstract_domain.valuation ->
state ->
state Eval.or_bottomstart_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.
stmt is the statement of the call site;call represents the call: the called function and the arguments;recursion is the information needed to interpret a recursive call.
It is None if the call is not recursive.state is the abstract state at the call site, before the call;valuation is a cache for all values and locations computed during
the evaluation of the function and its arguments.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_bottomfinalize_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.recursion is the information needed to interpret a recursive call.
It is None if the call is not recursive.pre and post are the states before and at the end of the call
respectively.val show_expr : (value, location,
origin)
Abstract_domain.valuation ->
state ->
Stdlib.Format.formatter -> Cil_types.exp -> unitCalled 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.