E_ACSL.Analyses_types
Types used by E-ACSL analyses
type lscope_var =
| Lvs_let of Frama_c_kernel.Cil_types.logic_var * Frama_c_kernel.Cil_types.term
| Lvs_quantif of Frama_c_kernel.Cil_types.term
* Frama_c_kernel.Cil_types.relation
* Frama_c_kernel.Cil_types.logic_var
* Frama_c_kernel.Cil_types.relation
* Frama_c_kernel.Cil_types.term
| Lvs_formal of Frama_c_kernel.Cil_types.logic_var
* Frama_c_kernel.Cil_types.logic_info
| Lvs_global of Frama_c_kernel.Cil_types.logic_var
* Frama_c_kernel.Cil_types.term
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 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
val pp_ival : Stdlib.Format.formatter -> ival -> unit
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
Type of a string that represents a number. Used when a string is required to encode a constant number because it is not representable in any C type
val pp_strnum : Stdlib.Format.formatter -> strnum -> unit