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 -> 'a
valid
: 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 process
val spawn : unit process
val 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 -> unit
val 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 -> unit
val get : Wpo.t -> [ `Script | `Proof | `Saved | `None ]