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