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 reset : tree -> unit
Sourceval clear : Wpo.t -> unit
Sourceval validate : tree -> unit

Re-compute stats & set status of the entire script

Sourceval consolidated : Wpo.t -> Stats.stats

Consolidate statistics wrt current script or prover results

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 proved : node -> bool
Sourceval pending : node -> int
Sourceval stats : node -> Stats.stats
Sourceval parent : node -> node option
Sourceval depth : node -> int
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 cancel : tree -> unit
Sourceval remove : tree -> node -> 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 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