module LogicUsage:sig
..end
val basename : Cil_types.varinfo -> string
Trims the original name
type
logic_lemma = {
|
lem_name : |
|||
|
lem_position : |
|||
|
lem_axiom : |
|||
|
lem_types : |
|||
|
lem_labels : |
|||
|
lem_property : |
|||
|
lem_depends : |
(* | in reverse order | *) |
type
axiomatic = {
|
ax_name : |
|
ax_position : |
|
ax_property : |
|
mutable ax_types : |
|
mutable ax_logics : |
|
mutable ax_lemmas : |
|
mutable ax_reads : |
type
logic_section =
| |
Toplevel of |
| |
Axiomatic of |
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 -> Wp.Clabels.LabelSet.t Wp.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 : Stdlib.Format.formatter -> Cil_types.logic_info -> unit
val dump : unit -> unit
Print on output