sig
  val basename : Cil_types.varinfo -> string
  type logic_lemma = {
    lem_name : string;
    lem_position : Lexing.position;
    lem_axiom : bool;
    lem_types : string list;
    lem_labels : Cil_types.logic_label list;
    lem_property : Cil_types.predicate;
    lem_depends : Wp.LogicUsage.logic_lemma list;
  }
  type axiomatic = {
    ax_name : string;
    ax_position : Lexing.position;
    ax_property : Property.t;
    mutable ax_types : Cil_types.logic_type_info list;
    mutable ax_logics : Cil_types.logic_info list;
    mutable ax_lemmas : Wp.LogicUsage.logic_lemma list;
    mutable ax_reads : Cil_datatype.Varinfo.Set.t;
  }
  type logic_section = Toplevel of int | Axiomatic of Wp.LogicUsage.axiomatic
  val compute : unit -> unit
  val ip_lemma : Wp.LogicUsage.logic_lemma -> Property.t
  val iter_lemmas : (Wp.LogicUsage.logic_lemma -> unit) -> unit
  val logic_lemma : string -> Wp.LogicUsage.logic_lemma
  val axiomatic : string -> Wp.LogicUsage.axiomatic
  val section_of_lemma : string -> Wp.LogicUsage.logic_section
  val section_of_type :
    Cil_types.logic_type_info -> Wp.LogicUsage.logic_section
  val section_of_logic : Cil_types.logic_info -> Wp.LogicUsage.logic_section
  val proof_context : unit -> Wp.LogicUsage.logic_lemma list
  val is_recursive : Cil_types.logic_info -> bool
  val get_induction_labels :
    Cil_types.logic_info ->
    string -> Wp.Clabels.LabelSet.t Wp.Clabels.LabelMap.t
  val get_name : Cil_types.logic_info -> string
  val pp_profile : Format.formatter -> Cil_types.logic_info -> unit
  val dump : unit -> unit
end