Module `Wp.LogicUsage`Source

Sourceval basename : Frama_c_kernel.Cil_types.varinfo -> string

Trims the original name

Sourcetype logic_lemma = {

}

Sourcetype axiomatic = {

}

Sourcetype logic_section =

Sourceval compute : unit -> unit

To force computation

Sourceval ip_lemma : logic_lemma -> Frama_c_kernel.Property.t

Sourceval iter_lemmas : (logic_lemma -> unit) -> unit

Sourceval fold_lemmas : (logic_lemma -> 'a -> 'a) -> 'a -> 'a

Sourceval logic_lemma : string -> logic_lemma

Sourceval axiomatic : string -> axiomatic

Sourceval section_of_lemma : string -> logic_section

Sourceval section_of_type : Frama_c_kernel.Cil_types.logic_type_info -> logic_section

Sourceval section_of_logic : Frama_c_kernel.Cil_types.logic_info -> logic_section

Sourceval proof_context : unit -> logic_lemma list

Lemmas that are not in an axiomatic.

Sourceval is_recursive : Frama_c_kernel.Cil_types.logic_info -> bool

val get_induction_labels : 
  Frama_c_kernel.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].

Sourceval get_name : Frama_c_kernel.Cil_types.logic_info -> string

val pp_profile : 
  Format.formatter ->
  Frama_c_kernel.Cil_types.logic_info ->
  unit

Sourceval dump : unit -> unit

Print on output

Install