module Register: sig
.. end
Do on_server_stop save why3 session
val job_key : Log.category
val cmdline : unit -> Factory.setup
val set_model : Factory.setup -> unit
val computer : unit -> Generator.computer
module Models: Model.S.Set
module Fmap: Kernel_function.Map
val wp_iter_model : ?ip:Property.t ->
?index:Wpo.index -> (Fmap.key -> Models.elt -> unit) -> unit
val wp_print_separation : Format.formatter -> unit
val do_wp_print : unit -> unit
val do_wp_print_for : Wpo.t Bag.t -> unit
val do_wp_report : unit -> unit
val already_valid : Wpo.t -> bool
val pp_warnings : Format.formatter -> Wpo.t -> unit
val auto_check : Wpo.t -> bool
val launch : 'a Task.task -> unit
val do_wpo_display : Wpo.t -> unit
module PM: FCMap.Make
(
sig
end
)
type
pstat = {
|
mutable proved : int ; |
|
mutable unknown : int ; |
|
mutable interrupted : int ; |
|
mutable failed : int ; |
|
mutable n_time : int ; |
|
mutable a_time : float ; |
|
mutable u_time : float ; |
|
mutable d_time : float ; |
|
mutable steps : int ; |
}
module GOALS: Wpo.S.Set
val scheduled : int Pervasives.ref
val exercised : int Pervasives.ref
val spy : bool Pervasives.ref
val session : GOALS.t Pervasives.ref
val proved : GOALS.t Pervasives.ref
val provers : pstat PM.t Pervasives.ref
val begin_session : unit -> unit
val clear_session : unit -> unit
val end_session : unit -> unit
val iter_session : (GOALS.elt -> unit) -> unit
val clear_scheduled : unit -> unit
val get_pstat : PM.key -> pstat
val add_step : pstat -> int -> unit
val add_time : pstat -> float -> unit
val do_list_scheduled : ((GOALS.elt -> unit) -> 'a) -> unit
val do_wpo_start : Wpo.t -> unit
val do_wpo_wait : unit -> unit
val do_wpo_prover : Wpo.t -> 'a -> unit
val do_wpo_stat : GOALS.elt -> PM.key -> VCS.result -> unit
val do_wpo_result : GOALS.elt -> PM.key -> VCS.result -> unit
val do_why3_result : GOALS.elt -> PM.key -> VCS.result -> unit
val do_wpo_success : Wpo.t -> VCS.prover option -> unit
val do_list_scheduled_result : unit -> unit
val spawn_wp_proofs_iter : provers:(VCS.mode * VCS.prover) list -> ((Wpo.t -> unit) -> 'a) -> unit
val get_prover_names : unit -> Wp_parameters.Provers.t
val compute_provers : bool Pervasives.ref -> unit -> (VCS.mode * VCS.prover) list
val do_wp_proofs_iter : ((GOALS.elt -> unit) -> unit) -> unit
val do_wp_proofs : unit -> unit
val do_wp_proofs_for : GOALS.elt Bag.t -> unit
val deprecated_wp_compute : Kernel_function.t option -> string list -> Property.t option -> unit
val deprecated_wp_compute_kf : Kernel_function.t option -> string list -> string list -> unit
val deprecated_wp_compute_ip : Property.t -> unit
val deprecated_wp_compute_call : Cil_types.stmt -> unit
val deprecated_wp_clear : unit -> unit
val cmdline_run : unit -> unit
val deprecated : string -> unit
val register : string -> ('a -> 'b) Type.t -> ('a -> 'b) -> unit
val run : unit -> unit
val pp_wp_parameters : Format.formatter -> unit
val do_prover_detect : unit -> unit
val try_sequence : (unit -> unit) list -> unit -> unit
val sequence : (unit -> unit) list -> unit -> unit
val tracelog : unit -> unit
val main : unit -> unit