module VCS: sig
.. end
Verification Condition Status
Prover
type
prover =
| |
Why3 of Why3Provers.t |
| |
NativeAltErgo |
| |
NativeCoq |
| |
Qed |
| |
Tactical |
type
mode =
| |
BatchMode |
| |
EditMode |
| |
FixMode |
module Pset: Set.S
with type elt = prover
module Pmap: Map.S
with type key = prover
val name_of_prover : prover -> string
val title_of_prover : prover -> string
val filename_for_prover : prover -> string
val prover_of_name : string -> prover option
val mode_of_prover_name : string -> mode
val title_of_mode : mode -> string
val pp_prover : Format.formatter -> prover -> unit
val pp_mode : Format.formatter -> mode -> unit
val cmp_prover : prover -> prover -> int
Config
None
means current WP option default.
Some 0
means prover default.
type
config = {
|
valid : bool ; |
|
timeout : int option ; |
|
stepout : int option ; |
}
val current : unit -> config
Current parameters
val default : config
all None
val get_timeout : config -> int
0 means no-timeout
val get_stepout : config -> int
0 means no-stepout
Results
type
verdict =
| |
NoResult |
| |
Invalid |
| |
Unknown |
| |
Timeout |
| |
Stepout |
| |
Computing of (unit -> unit) |
| |
Checked |
| |
Valid |
| |
Failed |
type
result = {
|
verdict : verdict ; |
|
cached : bool ; |
|
solver_time : float ; |
|
prover_time : float ; |
|
prover_steps : int ; |
|
prover_errpos : Lexing.position option ; |
|
prover_errmsg : string ; |
}
val no_result : result
val valid : result
val checked : result
val invalid : result
val unknown : result
val stepout : int -> result
val timeout : int -> result
val computing : (unit -> unit) -> result
val failed : ?pos:Lexing.position -> string -> result
val kfailed : ?pos:Lexing.position ->
('a, Format.formatter, unit, result) Pervasives.format4 -> 'a
val cached : result -> result
only for true verdicts
val result : ?cached:bool ->
?solver:float -> ?time:float -> ?steps:int -> verdict -> result
val is_auto : prover -> bool
val is_verdict : result -> bool
val is_valid : result -> bool
val is_computing : result -> bool
val configure : result -> config
val autofit : result -> bool
Result that fits the default configuration
val pp_result : Format.formatter -> result -> unit
val pp_result_perf : Format.formatter -> result -> unit
val compare : result -> result -> int
val merge : result -> result -> result
val choose : result -> result -> result
val best : result list -> result
val dkey_no_time_info : Wp.Wp_parameters.category
val dkey_no_step_info : Wp.Wp_parameters.category
val dkey_no_goals_info : Wp.Wp_parameters.category
val dkey_no_cache_info : Wp.Wp_parameters.category
val dkey_success_only : Wp.Wp_parameters.category