Module Analyses_types

module Analyses_types: sig .. end

Types used by E-ACSL analyses


type lscope_var = 
| Lvs_let of Cil_types.logic_var * Cil_types.term
| Lvs_quantif of Cil_types.term * Cil_types.relation * Cil_types.logic_var
* Cil_types.relation * Cil_types.term
| Lvs_formal of Cil_types.logic_var * Cil_types.logic_info
| Lvs_global of Cil_types.logic_var * Cil_types.term
type lscope = lscope_var list 
type pred_or_term = 
| PoT_pred of Cil_types.predicate
| PoT_term of Cil_types.term
type at_data = {
   kf : Cil_types.kernel_function; (*

kernel_function englobing the pred_or_term.

*)
   kinstr : 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 : 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