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