Module Register

module Register: sig .. end
Do on_server_stop save why3 session

val dkey_main : Wp_parameters.category
val dkey_raised : Wp_parameters.category
val dkey_shell : Wp_parameters.category
val cmdline : unit -> Factory.setup
val set_model : Factory.setup -> unit
val computer : unit -> Generator.computer
module Models: Set.Make(WpContext.MODEL)
module Fmap: Kernel_function.Map
val wp_iter_model : ?ip:Property.t ->
?index:Wpo.index -> (Fmap.key -> Models.elt -> unit) -> unit
val wp_print_memory_context : Kernel_function.t ->
WpContext.MODEL.t -> MemoryContext.clause list -> Format.formatter -> unit
val wp_warn_memory_context : unit -> unit
val do_wp_print : unit -> unit
val do_wp_print_for : Wpo.t Bag.t -> unit
val do_wp_report : unit -> unit
val pp_warnings : Format.formatter -> Wpo.t -> unit
val launch : 'a Task.task -> 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 interrupted : int;
   mutable incache : 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 dkey_prover : Wp_parameters.category
val do_wpo_start : Wpo.t -> unit
val do_wpo_wait : unit -> unit
val do_progress : Wpo.t -> string -> unit
val do_report_cache_usage : ProverWhy3.mode -> 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_wpo_success : Wpo.t -> VCS.prover option -> unit
val do_report_time : Format.formatter -> pstat -> unit
val do_report_steps : Format.formatter -> pstat -> unit
val do_report_stopped : Format.formatter -> pstat -> unit
val do_report_prover_stats : (Format.formatter -> string -> unit) ->
Format.formatter -> VCS.prover * pstat -> unit
val do_report_scheduled : unit -> unit
val do_list_scheduled_result : unit -> unit
type mode = {
   mutable tactical : bool;
   mutable update : bool;
   mutable depth : int;
   mutable width : int;
   mutable backtrack : int;
   mutable auto : Strategy.heuristic list;
   mutable provers : (VCS.mode * VCS.prover) list;
}
val spawn_wp_proofs_iter : mode:mode -> ((Wpo.t -> unit) -> 'a) -> unit
val get_prover_names : unit -> Wp_parameters.Provers.t
val compute_provers : mode:mode -> unit
val dump_strategies : unit -> unit
val default_mode : unit -> mode
val compute_auto : mode:mode -> unit
val do_update_session : mode -> ((Wpo.t -> unit) -> 'a) -> unit
val do_wp_proofs_iter : ?provers:Why3Provers.t list ->
?tip:bool -> ((GOALS.elt -> unit) -> unit) -> unit
val do_wp_proofs : unit -> unit
val do_wp_proofs_for : GOALS.elt Bag.t -> unit
val do_cache_cleanup : unit -> 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 dkey_logicusage : Wp_parameters.category
val dkey_refusage : Wp_parameters.category
val dkey_builtins : Wp_parameters.category
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