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 ->
(value, location,
origin)
Abstract_domain.valuation ->
state ->
state Eval.or_bottom
start_call stmt call 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;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.val finalize_call : Cil_types.stmt ->
(location, 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 show_expr : (value, location,
origin)
Abstract_domain.valuation ->
state ->
Stdlib.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.