ProverScript (frama-c-wp.Wp.ProverScript)

type 'a process =
  ?valid:bool ->
  ?failed:bool ->
  ?provers:VCS.prover list ->
  ?depth:int ->
  ?width:int ->
  ?backtrack:int ->
  ?auto:Strategy.heuristic list ->
  ?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)
provers: Additional list of provers to try when stuck
depth: 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 get : Wpo.t -> [ `Script | `Proof | `Saved | `None ]

val save : stdout:bool -> Wpo.t -> unit