module Analyses_types:sig
..end
Types used by E-ACSL analyses
type
lscope_var =
| |
Lvs_let of |
| |
Lvs_quantif of |
| |
Lvs_formal of |
| |
Lvs_global of |
typelscope =
lscope_var list
type
pred_or_term =
| |
PoT_pred of |
| |
PoT_term of |
type
at_data = {
|
kf : |
(* |
| *) |
|
kinstr : |
(* |
| *) |
|
lscope : |
(* | Current state of the | *) |
|
pot : |
(* |
| *) |
|
label : |
(* | Label of the | *) |
|
error : |
(* | Error raised during the pre-analysis.
This field does not contribute to the equality and comparison between two
| *) |
}
Type uniquely representing a predicate
or term
with an associated
label
, and the necessary information for its translation.
type
annotation_kind =
| |
Assertion |
| |
Precondition |
| |
Postcondition |
| |
Invariant |
| |
Variant |
| |
RTE |