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

Re-compute stats & set status of the entire script

val consolidated : Wpo.t -> Stats.stats

Consolidate statistics wrt current script or prover results

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