package frama-c

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

Module Wp.ProofEngineSource

Interactive Proof Engine

Sourcetype tree

A proof tree

Sourcetype node

A proof node

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

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

Sourceval consolidate : Wpo.t -> unit

Consolidate proof tree (memoized).

Sourceval consolidated : Wpo.t -> Stats.stats

Consolidated statistics (memoized).

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

Consolidated results (memoized).

Leaves are numbered from 0 to n-1

Sourcetype 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

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