sig
val basename : Cil_types.varinfo -> string
type logic_lemma = {
lem_name : string;
lem_position : Filepath.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 : Filepath.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 : Stdlib.Format.formatter -> Cil_types.logic_info -> unit
val dump : unit -> unit
end