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 return = return
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
state
type
return
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 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 assignement: Assign for
the default assignment of the value, or Copy for the exact copy of a
location if the right expresssion 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, return,
value)
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 make_return : Cil_types.kernel_function ->
Cil_types.stmt ->
value Eval.assigned ->
valuation ->
state -> return
make_return kf stmt assigned valuation state
makes an abstraction of the
return value of the function kf
.
stmt
is the return statement of kf
and state
the state of the
domain at this statement. assigned
represents the value of the lvalue
being returned, and valuation
is the valuation resulting from its
evaluation.
The return abstraction computed by this function can then be used for
the assignment at the call site.
val assign_return : Cil_types.stmt ->
location Eval.left_value ->
Cil_types.kernel_function ->
return ->
value Eval.assigned ->
valuation ->
state ->
state Eval.or_bottom
assign_return stmt lv kf return value valuation state
models on states
the effect of the assignment of the return value of a called function at
the call site.
stmt
is the statement of the call;
lv
is the lvalue being assigned, with its type and location;
kf
is the called function, whose return is assigned;
return
is an abstraction of this return, computed by make_return;
value
is a value abstraction for this return, computed by a standard
evaluation in the called function kf
;
valuation
results from the evaluation of the location of lv
;
state
is the state before the assignment, but after the call.
val default_call : Cil_types.stmt ->
value Eval.call ->
state ->
(state, return,
value)
Eval.call_result
val enter_loop : Cil_types.stmt ->
state -> state
val incr_loop_counter : Cil_types.stmt ->
state -> state
val leave_loop : Cil_types.stmt ->
state -> state