Module LogicUsage

module LogicUsage: sig .. end
Trims the original name

val basename : Cil_types.varinfo -> string
Trims the original name
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 Cil_types.named;
   lem_depends : logic_lemma list; (*
in reverse order
*)
}
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 : logic_lemma list;
   mutable ax_reads : Cil_datatype.Varinfo.Set.t;
}
type logic_section = 
| Toplevel of int
| Axiomatic of axiomatic
val compute : unit -> unit
To force computation
val ip_lemma : logic_lemma -> Property.t
val iter_lemmas : (logic_lemma -> unit) -> unit
val logic_lemma : string -> logic_lemma
val axiomatic : string -> axiomatic
val section_of_lemma : string -> logic_section
val section_of_type : Cil_types.logic_type_info -> logic_section
val section_of_logic : Cil_types.logic_info -> logic_section
val proof_context : unit -> logic_lemma list
Lemmas that are not in an axiomatic.
val is_recursive : Cil_types.logic_info -> bool
val get_induction_labels : Cil_types.logic_info -> string -> Clabels.LabelSet.t Clabels.LabelMap.t
Given an inductive phi{...A...}. Whenever in case C{...B...} we have a call to phi{...B...}, then A belongs to (induction phi C).[B].
val get_name : Cil_types.logic_info -> string
val pp_profile : Format.formatter -> Cil_types.logic_info -> unit
val dump : unit -> unit
Print on output