package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Wp.LogicUsageSource

Trims the original name

Sourcetype logic_lemma = {
  1. lem_loc : Frama_c_kernel.Cil_types.location;
  2. lem_name : string;
  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;
}
Sourcetype 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;
}
Sourcetype logic_section =
  1. | Toplevel of int
  2. | Axiomatic of axiomatic
Sourceval compute : unit -> unit

To force computation

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

Lemmas that are not in an axiomatic.

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 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