Module E_ACSL.Analyses_types

Types used by E-ACSL analyses

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

    kernel_function englobing the pred_or_term.

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

    kinstr where the pred_or_term is used.

    *)
  3. lscope : lscope;
    (*

    Current state of the lscope for the pred_or_term.

    *)
  4. pot : pred_or_term;
    (*

    pred_or_term to translate.

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

    Label of the pred_or_term.

    *)
  6. 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 =
  1. | Assertion
  2. | Precondition
  3. | Postcondition
  4. | Invariant
  5. | Variant
  6. | RTE
type ival =
  1. | Ival of Frama_c_kernel.Ival.t
  2. | Float of Frama_c_kernel.Cil_types.fkind * float option
  3. | Rational
  4. | Real
  5. | Nan

Type of intervals inferred by the interval inference

val pp_ival : Stdlib.Format.formatter -> ival -> unit
type number_ty =
  1. | C_integer of Frama_c_kernel.Cil_types.ikind
  2. | C_float of Frama_c_kernel.Cil_types.fkind
  3. | Gmpz
  4. | Rational
  5. | Real
  6. | Nan

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

type strnum =
  1. | Str_Z
  2. | Str_R
  3. | C_number

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