module LogicUsage: sig
.. end
Trims the original name
val basename : Cil_types.varinfo -> string
Trims the original name
type
logic_lemma = {
}
type
axiomatic = {
}
type
logic_section =
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