module Eval:sig
..end
include Bottom.Type
type'a
or_top =[ `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 ]
typeunop_context =
Cil_types.exp * Cil_types.exp
typebinop_context =
Cil_types.exp * Cil_types.exp * Cil_types.exp * Cil_types.typ
typeindex_context =
Cil_types.exp * Cil_types.offset * Cil_types.typ * Cil_types.exp option
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 : |
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
copied =
| |
Determinate of |
(* |
Determinates the right value before the copy:
the copied value is initialized, and without escaping addresses.
| *) |
| |
Exact of |
(* |
Exact copy of the right value, with possible indeterminateness
(then, the value can be bottom).
| *) |
type 'value
assigned =
| |
Assign of |
(* |
Default assignment of a value.
| *) |
| |
Copy of |
(* |
Used when the right expression of an assignment is a left value.
Copy the location of the lvalue
lval , that contains the value
value copied . The copy can remove or not the possible indeterminateness
of the value (according to the parameters of the analysis). | *) |
val value_assigned : 'value assigned -> 'value or_bottom
type 'value
argument = {
|
formal : |
|
concrete : |
|
avalue : |
type 'value
call = {
|
kf : |
|
arguments : |
|
rest : |
type ('state, 'summary, 'value)
return = {
|
post_state : |
|
returned_value : |
|
summary : |
type('state, 'summary, 'value)
call_result =('state, 'summary, 'value) return list or_bottom
type 't
init =
| |
Default |
(* |
The entry point is initialized to top, and all the others to bottom.
| *) |
| |
Continue of |
(* |
The entry point is initialized to the current value,
and all the others to bottom.
| *) |
| |
Custom of |
(* |
Custom association list for the initial values of statements. Other
statements are initialized to bottom.
| *) |
type ('state, 'summary, 'value)
action =
| |
Compute of |
(* |
Analyze the called function with the given initialization. If the summary
of a previous analysis for this initialization has been cached, it will
be used without re-computation.
The second boolean indicates whether the result must be cached.
| *) |
| |
Recall of |
(* |
Do not run the analysis of the function, but use the summary for this
initialization if it exists. Otherwise,
default_call is called. | *) |
| |
Result of |
(* |
Direct computation of the result.
| *) |
exception InvalidCall