Frama-C API - ProverTask
class printer : Stdlib.Format.formatter -> string -> object ... end
val pp_file : message:string -> file:Frama_c_kernel.Filepath.Normalized.t -> unit
class type pattern = object ... end
never fails
class virtual command : string -> object ... end
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 schedule : 'a Frama_c_kernel.Task.task -> unit
val spawn : ?monitor:('a option -> unit) -> ?pool:Frama_c_kernel.Task.pool -> all:bool -> smoke:bool -> ('a * bool Frama_c_kernel.Task.task) list -> unit
Spawn all the tasks over the server and retain the first 'validated' one. The callback monitor
is called with Some
at first success, and None
if none succeed. An option pool
task can be passed to register the associated threads.