Frama-C:
Plug-ins:
Libraries:

Frama-C API - Prover

val simplify : ?start:(Wpo.t -> unit) -> ?result:(Wpo.t -> VCS.prover -> VCS.result -> unit) -> ?commit:bool -> 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