Frama-C:
Plug-ins:
Libraries:

Frama-C API - ProverTask

val server : ?procs:int -> unit -> Frama_c_kernel.Task.server

If provided, the number of procs is forwarded to the Why3 and the server

val simplify : ?start:(Wpo.t -> unit) -> ?result:(Wpo.t -> Prover.t -> VCS.result -> unit) -> ?commit:bool -> Wpo.t -> bool Frama_c_kernel.Task.task
val prove : Wpo.t -> ?config:VCS.config -> ?mode:Prover.InteractiveMode.t -> ?start:(Wpo.t -> unit) -> ?progress:(Wpo.t -> string -> unit) -> ?result:(Wpo.t -> Prover.t -> VCS.result -> unit) -> Prover.t -> 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 -> Prover.t -> VCS.result -> unit) -> ?success:(Wpo.t -> Prover.t option -> unit) -> (Prover.InteractiveMode.t * Prover.t) list -> unit