Frama-C:
Plug-ins:
Libraries:

Frama-C API - ProverWhy3

val prove : ?mode:Prover.InteractiveMode.t -> ?timeout:float -> ?steplimit:int -> ?memlimit:int -> prover:Why3Env.prover -> Wpo.t -> VCS.result Frama_c_kernel.Task.task

Return NoResult if it is already proved by Qed