package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type
val basename : Frama_c_kernel.Cil_types.varinfo -> string

Trims the original name

type logic_lemma = {
  1. lem_name : string;
  2. lem_position : Frama_c_kernel.Filepath.position;
  3. lem_types : string list;
  4. lem_labels : Frama_c_kernel.Cil_types.logic_label list;
  5. lem_predicate : Frama_c_kernel.Cil_types.toplevel_predicate;
  6. lem_depends : logic_lemma list;
    (*

    in reverse order

    *)
  7. lem_attrs : Frama_c_kernel.Cil_types.attributes;
}
type axiomatic = {
  1. ax_name : string;
  2. ax_position : Frama_c_kernel.Filepath.position;
  3. ax_property : Frama_c_kernel.Property.t;
  4. mutable ax_types : Frama_c_kernel.Cil_types.logic_type_info list;
  5. mutable ax_logics : Frama_c_kernel.Cil_types.logic_info list;
  6. mutable ax_lemmas : logic_lemma list;
  7. mutable ax_reads : Frama_c_kernel.Cil_datatype.Varinfo.Set.t;
}
type logic_section =
  1. | Toplevel of int
  2. | Axiomatic of axiomatic
val compute : unit -> unit

To force computation

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 proof_context : unit -> logic_lemma list

Lemmas that are not in an axiomatic.

val is_recursive : Frama_c_kernel.Cil_types.logic_info -> bool
val get_induction_labels : Frama_c_kernel.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 : Frama_c_kernel.Cil_types.logic_info -> string
val pp_profile : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.logic_info -> unit
val dump : unit -> unit

Print on output

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct