Wp.Prover
val simplify :
?start:( Wpo.t -> unit ) ->
?result:( Wpo.t -> VCS.prover -> VCS.result -> unit ) ->
Wpo.t ->
bool Frama_c_kernel.Task.task
val prove :
Wpo.t ->
?config:VCS.config ->
?mode:VCS.mode ->
?start:( Wpo.t -> unit ) ->
?progress:( Wpo.t -> string -> unit ) ->
?result:( Wpo.t -> VCS.prover -> VCS.result -> unit ) ->
VCS.prover ->
bool Frama_c_kernel.Task.task
val spawn :
Wpo.t ->
delayed:bool ->
?config:VCS.config ->
?start:( Wpo.t -> unit ) ->
?progress:( Wpo.t -> string -> unit ) ->
?result:( Wpo.t -> VCS.prover -> VCS.result -> unit ) ->
?success:( Wpo.t -> VCS.prover option -> unit ) ->
?pool:Frama_c_kernel.Task.pool ->
(VCS.mode * VCS.prover) list ->
unit