sig
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 = Analyses_types.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;
kinstr : Cil_types.kinstr;
lscope : Analyses_types.lscope;
pot : Analyses_types.pred_or_term;
label : Cil_types.logic_label;
error : exn option;
}
type annotation_kind =
Assertion
| Precondition
| Postcondition
| Invariant
| Variant
| RTE
end