Frama-C API - ProofEngine
Interactive Proof Engine
module Node : sig ... end
val get : Wpo.t -> [ `Script | `Proof | `Saved | `None ]
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
val pool : tree -> Lang.F.pool
val saved : tree -> bool
val set_saved : tree -> bool -> unit
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 tactic : node -> Tactical.t option
val child_label : node -> string option
val tactic_label : node -> string option
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 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
val fork : tree -> anchor:node -> ProofScript.jtactic -> Tactical.process -> fork
val pretty : Stdlib.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