module type Transfer = sig
.. end
Transfer function of the domain.
type
state
type
summary
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 cached in valuation
.
val assign : Cil_types.kinstr ->
location Eval.left_value ->
Cil_types.exp ->
value Eval.assigned ->
valuation ->
state ->
state Eval.or_bottom
assign lv expr v valuation state
is the transfer function for the
assignment lv = expr
in state
. It must return the state where the
assignment has been performed. v
is the value corresponding to
the already-evaluated expression exp
.
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 exp bool valuation state
returns a state in which the boolean
expression exp
evaluates to bool
.
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 call_action : Cil_types.stmt ->
value Eval.call ->
valuation ->
state ->
(state, summary,
value)
Eval.action
Decision on a function call:
call_action stmt call valuation state
decides on the analysis of
the called function; see for details on the action type,
which described the analysis.
stmt
is the statement of the call, call
represents the call
(the called function and the arguments) and state
the state before
the call.
val summarize : Cil_types.kernel_function ->
Cil_types.stmt ->
returned:(location Eval.left_value *
value Eval.copied)
option ->
state ->
(summary * state)
Eval.or_bottom
summarize kf stmt ~returned_lv state
returns a summary of the
state state
at the end of the function kf
. This summary will be
used at the call site for the analysis of the calling function.
stmt
is the return statement of kf
, and returned_lv
is None if no
value is returned, or represents the return lvalue, its type and
its location (see for details).
val resolve_call : Cil_types.stmt ->
value Eval.call ->
assigned:(location Eval.left_value *
value Eval.copied)
option ->
valuation ->
pre:state ->
post:summary * state ->
state Eval.or_bottom
resolve_call stmt ~assigned_lv call valuation ~pre_state ~post_state
compute the state after the statement
stmt
where the lvalue
assigned
is assigned to the result of the call
call
.
stmt
is the statement of the call;
assigned_lv
is None if no variable is assigned, or is the assigned
lvalue, its type and its location (see for details);
call
represents the function call and its arguments;
pre_state
is the state before the call;
post_state
is the state at the end of the called function, and
the summary computed by the summarize
function above.
val default_call : Cil_types.stmt ->
value Eval.call ->
state ->
(state, summary,
value)
Eval.call_result