Module Register

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
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_result : Wpo.t -> Format.formatter -> VCS.result -> unit
val do_wpo_start : Wpo.t -> VCS.prover -> unit
val auto_check_valid : Wpo.t -> VCS.result -> bool
val is_verdict : VCS.result -> bool
val wp_why3ide_launch : unit Task.task -> unit
val do_wp_check_iter : [< `Altergo | `Coq | `Why3 ] list -> ((Wpo.t -> unit) -> 'a) -> unit
val do_wp_check : unit -> unit
val do_wp_check_for : Wpo.t Bag.t -> unit
val do_wpo_display : Wpo.t -> unit
module PM: FCMap.Make(sig
type t = VCS.prover 
val compare : VCS.prover -> VCS.prover -> int
end)
type pstat = {
   mutable proved : int;
   mutable unknown : int;
   mutable interruped : int;
   mutable failed : int;
   mutable uptime : float;
   mutable dntime : float;
   mutable steps : int;
}
module GOALS: Wpo.S.Set
val scheduled : 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_feedback : GOALS.elt -> PM.key -> VCS.result -> unit
val do_list_scheduled_result : unit -> unit
val spwan_wp_proofs_iter : provers:(VCS.mode * VCS.prover) list -> ((Wpo.t -> unit) -> unit) -> 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 wp_compute_deprecated : Kernel_function.t option -> string list -> Property.t option -> unit
val wp_compute_kf : Kernel_function.t option ->
Datatype.String.t list -> Datatype.String.t list -> unit
val wp_compute_ip : Property.t -> unit
val wp_compute_call : Cil_datatype.Stmt.t -> unit
val wp_clear : unit -> unit
val cmdline_run : unit -> unit
val wp_compute : Kernel_function.t option ->
Datatype.String.t list -> Property.t option -> unit
val wp_compute_kf : Kernel_function.t option ->
Datatype.String.t list -> Datatype.String.t list -> unit
val wp_compute_ip : Property.t -> unit
val wp_compute_call : Cil_datatype.Stmt.t -> unit
val wp_clear : unit -> unit
val run : unit -> unit
val pp_wp_parameters : Format.formatter -> unit
val do_prover_detect : unit -> unit
val do_finally : (unit -> 'a) -> (unit -> unit) -> unit -> unit
val (&&&) : (unit -> 'a) -> (unit -> unit) -> unit -> unit
val sequence : (unit -> 'a) list -> unit -> unit
val tracelog : unit -> unit
val main : unit -> unit