module type Transfer =sig
..end
Transfer function of the domain.
type
state
type
value
type
location
type
origin
val update : (value, location,
origin)
Abstract_domain.valuation ->
state ->
state Eval.or_bottom
update 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_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.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_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 ->
(location, value) Eval.call ->
Eval.recursion option ->
(value, location,
origin)
Abstract_domain.valuation ->
state ->
state Eval.or_bottom
start_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_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.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 -> unit
Called 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.