package frama-c

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

Interactive Proof Engine

type tree

A proof tree

type node

A proof node

module Node : sig ... end
val get : Wpo.t -> [ `Script | `Proof | `Saved | `None ]
val proof : main:Wpo.t -> tree
val validate : tree -> unit

Consolidate and update status of the entire script (memoized).

val consolidate : Wpo.t -> unit

Consolidate proof tree (memoized).

val consolidated : Wpo.t -> Stats.stats

Consolidated statistics (memoized).

val results : Wpo.t -> (VCS.prover * VCS.result) list

Consolidated results (memoized).

Leaves are numbered from 0 to n-1

type status = [
  1. | `Unproved
    (*

    proof obligation not proved

    *)
  2. | `Proved
    (*

    proof obligation is proved

    *)
  3. | `Pending of int
    (*

    proof is pending

    *)
  4. | `Passed
    (*

    smoke test is passed (PO is not proved)

    *)
  5. | `Invalid
    (*

    smoke test has failed (PO is proved)

    *)
  6. | `StillResist of int
    (*

    proof is pending

    *)
]
type current = [
  1. | `Main
  2. | `Internal of node
  3. | `Leaf of int * node
]
type position = [
  1. | `Main
  2. | `Node of node
  3. | `Leaf of int
]
val pool : tree -> Lang.F.pool
val saved : tree -> bool
val set_saved : tree -> bool -> unit
val status : tree -> status
val current : tree -> current
val goto : tree -> position -> unit
val root : tree -> node
val main : tree -> Wpo.t
val goal : node -> Wpo.t
val tree : node -> tree
val head : tree -> node option
val head_goal : tree -> Wpo.t
val tree_context : tree -> WpContext.t
val node_context : node -> WpContext.t
val title : node -> string
val fully_proved : node -> bool
val locally_proved : node -> bool
val pending : node -> int
val stats : node -> Stats.stats
val depth : node -> int
val path : node -> node list
val parent : node -> node option
val tactic : node -> Tactical.t option
val child_label : node -> string option
val tactic_label : node -> string option
val subgoals : node -> node list
val children : node -> (string * node) list
val tactical : node -> ProofScript.jtactic option
val get_strategies : node -> int * Strategy.t array
val set_strategies : node -> ?index:int -> Strategy.t array -> unit
val get_hint : node -> string option
val set_hint : node -> string -> unit
val forward : tree -> unit
val clear_goal : Wpo.t -> unit
val clear_tree : tree -> unit
val clear_node : tree -> node -> unit
val clear_node_tactic : tree -> node -> unit
val clear_parent_tactic : tree -> node -> unit
val add_goal_hook : (Wpo.t -> unit) -> unit
val add_clear_hook : (Wpo.t -> unit) -> unit
val add_remove_hook : (node -> unit) -> unit
val add_update_hook : (node -> unit) -> unit
val cancel_parent_tactic : tree -> unit
val cancel_current_node : tree -> unit
type fork
val anchor : tree -> ?node:node -> unit -> node
val fork : tree -> anchor:node -> ProofScript.jtactic -> Tactical.process -> fork
val iter : (Wpo.t -> unit) -> fork -> unit
val commit : fork -> node * (string * node) list
val pretty : Format.formatter -> fork -> unit
val has_proof : Wpo.t -> bool
val has_script : tree -> bool
val script : tree -> ProofScript.jscript
val bind : node -> ProofScript.jscript -> unit
val bound : node -> ProofScript.jscript
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