E_ACSL.Analyses_types
Types used by E-ACSL analyses
type lscope_var =
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; | (*
|
kinstr : Frama_c_kernel.Cil_types.kinstr; | (*
|
lscope : lscope; | (* Current state of the |
pot : pred_or_term; | (*
|
label : Frama_c_kernel.Cil_types.logic_label; | (* Label of the |
error : exn option; | (* 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 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