Module E_ACSL.Analyses_types

Types used by E-ACSL analyses

type lscope = lscope_var list
type pred_or_term =
| PoT_pred of Frama_c_kernel.Cil_types.predicate
| PoT_term of Frama_c_kernel.Cil_types.term
type at_data = {
kf : Frama_c_kernel.Cil_types.kernel_function;(*

kernel_function englobing the pred_or_term.

*)
kinstr : Frama_c_kernel.Cil_types.kinstr;(*

kinstr where the pred_or_term is used.

*)
lscope : lscope;(*

Current state of the lscope for the pred_or_term.

*)
pot : pred_or_term;(*

pred_or_term to translate.

*)
label : Frama_c_kernel.Cil_types.logic_label;(*

Label of the pred_or_term.

*)
error : exn option;(*

Error raised during the pre-analysis. This field does not contribute to the equality and comparison between two at_data.

*)
}

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
type ival =
| Ival of Frama_c_kernel.Ival.t
| Float of Frama_c_kernel.Cil_types.fkind * float option
| Rational
| Real
| Nan

Type of intervals inferred by the interval inference

type number_ty =
| C_integer of Frama_c_kernel.Cil_types.ikind
| C_float of Frama_c_kernel.Cil_types.fkind
| Gmpz
| Rational
| Real
| Nan

Type of types inferred by the type inference for types representing numbers