module VCS:sig
..end
Verification Condition Status
type
prover =
| |
Why3 of |
(* | Prover via WHY | *) |
| |
NativeAltErgo |
(* | Direct Alt-Ergo | *) |
| |
NativeCoq |
(* | Direct Coq and Coqide | *) |
| |
Qed |
(* | Qed Solver | *) |
| |
Tactical |
(* | Interactive Prover | *) |
type
mode =
| |
Batch |
(* | Only check scripts | *) |
| |
Update |
(* | Check and update scripts | *) |
| |
Edit |
(* | Edit then check scripts | *) |
| |
Fix |
(* | Try check script, then edit script on non-success | *) |
| |
FixUpdate |
(* | Update & Fix | *) |
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 title_of_mode : mode -> string
val parse_mode : string -> mode
val parse_prover : string -> prover option
val pp_prover : Stdlib.Format.formatter -> prover -> unit
val pp_mode : Stdlib.Format.formatter -> mode -> unit
val cmp_prover : prover -> prover -> int
None
means current WP option default.
Some 0
means prover default.
type
config = {
|
valid : |
|
timeout : |
|
stepout : |
val current : unit -> config
Current parameters
val default : config
all None
val get_timeout : smoke:bool -> config -> int
0 means no-timeout
val get_stepout : config -> int
0 means no-stepout
type
verdict =
| |
NoResult |
| |
Invalid |
| |
Unknown |
| |
Timeout |
| |
Stepout |
| |
Computing of |
| |
Valid |
| |
Failed |
type
result = {
|
verdict : |
|
cached : |
|
solver_time : |
|
prover_time : |
|
prover_steps : |
|
prover_errpos : |
|
prover_errmsg : |
val no_result : result
val valid : result
val invalid : result
val unknown : result
val stepout : int -> result
val timeout : int -> result
val computing : (unit -> unit) -> result
val failed : ?pos:Stdlib.Lexing.position -> string -> result
val kfailed : ?pos:Stdlib.Lexing.position ->
('a, Stdlib.Format.formatter, unit, result) Stdlib.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 is_proved : smoke:bool -> result -> bool
val smoked : verdict -> verdict
val verdict : smoke:bool -> result -> verdict
val configure : result -> config
val autofit : result -> bool
Result that fits the default configuration
val pp_result : Stdlib.Format.formatter -> result -> unit
val pp_result_qualif : ?updating:bool -> prover -> result -> Stdlib.Format.formatter -> unit
val compare : result -> result -> int
val merge : result -> result -> result
val choose : result -> result -> result
val best : result list -> result
val dkey_shell : Wp_parameters.category