Module LogicUsage

module LogicUsage: sig .. end
Trims the original name

val trim : string -> 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 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 is_global_axiomatic : axiomatic -> bool
module SMap: Datatype.String.Map
module TMap: Cil_datatype.Logic_type_info.Map
module LMap: Cil_datatype.Logic_info.Map
module LSet: Cil_datatype.Logic_info.Set
type inductive_case = {
   ind_logic : Cil_types.logic_info;
   ind_case : string;
   mutable ind_call : Clabels.LabelSet.t Clabels.LabelMap.t;
}
type database = {
   mutable cases : inductive_case list LMap.t;
   mutable clash : LSet.t SMap.t;
   mutable names : string LMap.t;
   mutable types : logic_section TMap.t;
   mutable logics : logic_section LMap.t;
   mutable lemmas : (logic_lemma * logic_section) SMap.t;
   mutable recursives : LSet.t;
   mutable axiomatics : axiomatic SMap.t;
   mutable proofcontext : logic_lemma list;
}
val empty_database : unit -> database
module DatabaseType: Datatype.Make(sig
type t = LogicUsage.database 
include Datatype.Serializable_undefined
val reprs : LogicUsage.database list
val name : string
end)
module Database: State_builder.Ref(DatabaseType)(sig
val name : string
val dependencies : State.t list
val default : unit -> LogicUsage.database
end)
val pp_logic : Format.formatter -> Cil_types.logic_info -> unit
val basename : Cil_types.varinfo -> string
Trims the original name
val compute_logicname : LMap.key -> string
val is_overloaded : Cil_types.logic_info -> bool
val pp_profile : Format.formatter -> Cil_types.logic_info -> unit
val ip_lemma : logic_lemma -> Property.identified_property
val lemma_of_global : logic_lemma list ->
Cil_types.global_annotation -> logic_lemma
val populate : axiomatic ->
logic_lemma list -> Cil_types.global_annotation -> unit
val ip_of_axiomatic : Cil_types.global_annotation -> Property.identified_property
val axiomatic_of_global : logic_lemma list ->
Cil_types.global_annotation -> axiomatic
val register_logic : database -> logic_section -> LSet.elt -> unit
val register_lemma : database ->
logic_section -> logic_lemma -> unit
val register_type : database -> logic_section -> TMap.key -> unit
val register_axiomatic : database -> axiomatic -> unit
val register_cases : LMap.key -> inductive_case list -> unit
val add_call : Clabels.LabelSet.t Clabels.LabelMap.t ->
Cil_types.logic_label * Cil_types.logic_label ->
Clabels.LabelSet.t Clabels.LabelMap.t
class visitor : object .. end
val compute : unit -> unit
To force computation
val is_recursive : LSet.elt -> bool
val get_induction_labels : LMap.key -> 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 axiomatic : SMap.key -> axiomatic
val section_of_type : TMap.key -> logic_section
val section_of_logic : LMap.key -> logic_section
val get_lemma : SMap.key -> logic_lemma * logic_section
val iter_lemmas : (logic_lemma -> unit) -> unit
val logic_lemma : SMap.key -> logic_lemma
val section_of_lemma : SMap.key -> logic_section
val proof_context : unit -> logic_lemma list
Lemmas that are not in an axiomatic.
val dump_type : Format.formatter -> Cil_types.logic_type_info -> unit
val dump_profile : Format.formatter -> string -> LMap.key -> unit
val dump_logic : Format.formatter -> database -> LMap.key -> unit
val dump_lemma : Format.formatter -> logic_lemma -> unit
val get_name : LMap.key -> string
val pp_section : Format.formatter -> logic_section -> unit
val dump : unit -> unit
Print on output