module LogicUsage: sig
.. end
Trims the original name
val trim : string -> string
type
logic_lemma = {
}
type
axiomatic = {
}
type
logic_section =
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 = {
}
val empty_database : unit -> database
module DatabaseType: Datatype.Make
(
sig
end
)
module Database: State_builder.Ref
(
DatabaseType
)
(
sig
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