Frama-C API - ProverScript
type 'a process = ?valid:bool -> ?failed:bool -> ?scratch:bool -> ?provers:VCS.prover list -> ?depth:int -> ?width:int -> ?backtrack:int -> ?auto:Strategy.heuristic list -> ?strategies:bool -> ?start:(Wpo.t -> unit) -> ?progress:(Wpo.t -> string -> unit) -> ?result:(Wpo.t -> VCS.prover -> VCS.result -> unit) -> ?success:(Wpo.t -> VCS.prover option -> unit) -> Wpo.t -> 'avalid: Play provers with valid result (default: true)failed: Play provers with invalid result (default: true)scratch: Discard existing script (default: false)provers: Additional list of provers to try when stuckdepth: Strategy search depth (default: 0)width: Strategy search width (default: 0)backtrack: Strategy backtracking (default: 0)auto: Strategies to try (default: none)
val prove : unit Frama_c_kernel.Task.task processval spawn : unit processval search : ?depth:int -> ?width:int -> ?backtrack:int -> ?auto:Strategy.heuristic list -> ?provers:VCS.prover list -> ?progress:(Wpo.t -> string -> unit) -> ?result:(Wpo.t -> VCS.prover -> VCS.result -> unit) -> ?success:(Wpo.t -> VCS.prover option -> unit) -> ProofEngine.tree -> ProofEngine.node -> unitval explore : ?depth:int -> ?strategy:ProofStrategy.strategy -> ?progress:(Wpo.t -> string -> unit) -> ?result:(Wpo.t -> VCS.prover -> VCS.result -> unit) -> ?success:(Wpo.t -> VCS.prover option -> unit) -> ProofEngine.tree -> ProofEngine.node -> unitval get : Wpo.t -> [ `Script | `Proof | `Saved | `None ]