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 =