module Eval:sig
..end
include Bottom.Type
type'a
or_top =[ `Top | `Value of 'a ]
type'a
or_top_or_bottom =[ `Bottom | `Top | `Value of 'a ]
type't
with_alarms ='t * Alarmset.t
type't
evaluated ='t or_bottom with_alarms
val (>>=) : 'a evaluated -> ('a -> 'b evaluated) -> 'b evaluated
val (>>=.) : 'a evaluated -> ('a -> 'b or_bottom) -> 'b evaluated
val (>>=:) : 'a evaluated -> ('a -> 'b) -> 'b evaluated
type'a
reduced =[ `Bottom | `Unreduced | `Value of 'a ]
type
unop_context = {
|
operand : |
Context for the evaluation of an unary operator: contains the involved
expressions needed to create the appropriate alarms.
type
binop_context = {
|
left_operand : |
|
right_operand : |
|
binary_result : |
Context for the evaluation of a binary operator: contains the expressions
of both operands and of the result, needed to create the appropriate
alarms.
The origin of an abstract value is then provided by the abstract domain, and kept in the cache. The origin is None if the value has been internally computed without calling the domain.
Also, a value provided by the domain may be reduced by the internal computation of the forward and backward evaluation. Such a reduction is tracked by the evaluator and reported to the domain, in the cache. States of reduction are:
type
reductness =
| |
Unreduced |
(* |
No reduction.
| *) |
| |
Reduced |
(* |
A reduction has been performed for this expression.
| *) |
| |
Created |
(* |
The abstract value has been created.
| *) |
| |
Dull |
(* |
Reduction is pointless for this expression.
| *) |
type 'a
flagged_value = {
|
v : |
|
initialized : |
|
escaping : |
module Flagged_Value:sig
..end
type ('a, 'origin)
record_val = {
|
value : |
(* |
The resulting abstract value
| *) |
|
origin : |
(* |
The origin of the abstract value
| *) |
|
reductness : |
(* |
The state of reduction.
| *) |
|
val_alarms : |
(* |
The emitted alarms during the evaluation.
| *) |
type 'a
record_loc = {
|
loc : |
(* |
The location of the left-value.
| *) |
|
typ : |
(* | *) |
|
|
loc_alarms : |
(* |
The emitted alarms during the evaluation.
| *) |
module type Valuation =sig
..end
module Clear_Valuation:
type 'loc
left_value = {
|
lval : |
|
lloc : |
|
ltyp : |
type 'value
assigned =
| |
Assign of |
(* |
Default assignment of a value.
| *) |
| |
Copy of |
(* |
Copy of the location of the lvalue
lval , that contains the value
value copied . The value is copied exactly, with possible
indeterminateness. | *) |
val value_assigned : 'value assigned -> 'value or_bottom
type 'value
argument = {
|
formal : |
(* |
The formal argument of the called function.
| *) |
|
concrete : |
(* |
The concrete argument at the call site
| *) |
|
avalue : |
(* |
The value of the concrete argument.
| *) |
type 'value
call = {
|
kf : |
(* |
The called function.
| *) |
|
arguments : |
(* |
The arguments of the call.
| *) |
|
rest : |
(* |
Extra-arguments.
| *) |
|
return : |
(* |
Fake varinfo to store the return value
of the call.
| *) |
|
recursive : |
type 'state
call_action =
| |
Compute of |
(* |
Analyze the called function, starting with the given state at the
entry-point. If the summary of a previous analysis for this initialization
has been cached, it will be used without re-computation.
| *) |
| |
Result of |
(* |
Direct computation of the result.
| *) |
exception InvalidCall