module Register: sig
.. end
val dkey_main : Wp_parameters.category
val dkey_raised : Wp_parameters.category
val wkey_smoke : Wp_parameters.warn_category
val cmdline : unit -> Factory.setup
val set_model : Factory.setup -> unit
val computer : unit -> Generator.computer
module Models: Stdlib.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_compute_memory_context : WpContext.MODEL.t -> unit
val wp_warn_memory_context : WpContext.MODEL.t -> unit
val wp_insert_memory_context : WpContext.MODEL.t -> unit
val do_wp_print : unit -> unit
val do_wp_print_for : Wpo.t Bag.t -> unit
val do_wp_report : WpContext.MODEL.t -> unit
val pp_warnings : Stdlib.Format.formatter -> Wpo.t -> unit
val launch : 'a Task.task -> unit
val do_wpo_display : Wpo.t -> unit
module PM: Stdlib.Map.Make
(
sig
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 Stdlib.ref
val exercised : int Stdlib.ref
val session : GOALS.t Stdlib.ref
val provers : pstat PM.t Stdlib.ref
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 Bag.t -> 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 : Cache.mode -> unit
val do_wpo_stat : Wpo.t -> PM.key -> VCS.result -> unit
val do_wpo_result : Wpo.t -> PM.key -> VCS.result -> unit
val results : Wpo.t -> (VCS.prover * VCS.result) list
val do_wpo_failed : Wpo.t -> unit
val do_wpo_smoke : [< `Failed | `Passed | `Unknown ] -> Wpo.t -> unit
val do_wpo_success : Wpo.t -> VCS.prover option -> unit
val do_report_time : Stdlib.Format.formatter -> pstat -> unit
val do_report_steps : Stdlib.Format.formatter -> pstat -> unit
val do_report_stopped : Stdlib.Format.formatter -> pstat -> unit
val do_report_prover_stats : (Stdlib.Format.formatter -> string -> unit) ->
Stdlib.Format.formatter -> VCS.prover * pstat -> unit
val do_report_scheduled : unit -> unit
val do_list_scheduled_result : unit -> unit
type
script = {
|
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 : script:script -> Wpo.t Bag.t -> unit
val get_prover_names : unit -> Wp_parameters.Provers.t
val env_script_update : unit -> bool
val compute_provers : mode:VCS.mode -> script:script -> unit
val dump_strategies : unit -> unit
val default_script_mode : unit -> script
val compute_auto : script:script -> unit
val do_update_session : script:script -> Wpo.t Bag.t -> unit
val do_wp_proofs : ?provers:Why3Provers.t list -> ?tip:bool -> Wpo.t Bag.t -> unit
val do_cache_cleanup : 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 pp_wp_parameters : Stdlib.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