Module VCS
module VCS: sig
.. end
Verification Conditions Database
type
prover =
| |
Why3 of string |
| |
Why3ide |
| |
AltErgo |
| |
Coq |
| |
Qed |
type
mode =
| |
BatchMode |
| |
EditMode |
| |
FixMode |
type
language =
| |
L_why3 |
| |
L_coq |
| |
L_altergo |
val prover_of_name : string -> prover option
val name_of_prover : prover -> string
val name_of_mode : mode -> string
val sanitize_why3 : string -> string
val filename_for_prover : prover -> string
val language_of_name : string -> language option
val language_of_prover : prover -> language
val language_of_prover_name : string -> language option
val mode_of_prover_name : string -> mode
val cmp_prover : prover -> prover -> int
val pp_prover : Format.formatter -> prover -> unit
val pp_language : Format.formatter -> language -> unit
val pp_mode : Format.formatter -> mode -> unit
type
verdict =
| |
NoResult |
| |
Invalid |
| |
Unknown |
| |
Timeout |
| |
Stepout |
| |
Computing of (unit -> unit) |
| |
Valid |
| |
Failed |
type
result = {
|
verdict : verdict ; |
|
solver_time : float ; |
|
prover_time : float ; |
|
prover_steps : int ; |
|
prover_errpos : Lexing.position option ; |
|
prover_errmsg : string ; |
}
val result : ?solver:float -> ?time:float -> ?steps:int -> verdict -> result
val no_result : result
val valid : result
val invalid : result
val unknown : result
val timeout : result
val stepout : result
val computing : (unit -> unit) -> result
val failed : ?pos:Lexing.position -> string -> result
val pp_perf : Format.formatter -> result -> unit
val pp_result : Format.formatter -> result -> unit