package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

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

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