Module Wp.LogicUsage

module LogicUsage: sig .. end

val basename : Cil_types.varinfo -> string

Trims the original name

type logic_lemma = {

`lem_name : string;`
`lem_position : Filepath.position;`
`lem_types : string list;`
`lem_labels : Cil_types.logic_label list;`
`lem_predicate : Cil_types.toplevel_predicate;`
`lem_depends : logic_lemma list;`	`(*`	in reverse order	`*)`
`lem_attrs : Cil_types.attributes;`

}

type axiomatic = {

	`ax_name : string;`
	`ax_position : Filepath.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 fold_lemmas : (logic_lemma -> 'a -> 'a) -> 'a -> 'a

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