Module VCS

module VCS: sig .. end
Verification Condition Status


Prover


type prover = 
| Why3 of string
| Why3ide
| AltErgo
| Coq
| Qed
| Tactical
type mode = 
| BatchMode
| EditMode
| FixMode
type language = 
| L_why3
| L_coq
| L_altergo
module Pset: Set.S  with type elt = prover
module Pmap: Map.S  with type key = prover
val language_of_prover : prover -> language
val language_of_name : string -> language option
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 language_of_prover_name : string -> language option
val mode_of_prover_name : string -> mode
val title_of_mode : mode -> string
val pp_prover : Format.formatter -> prover -> unit
val pp_language : Format.formatter -> language -> 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;
   depth : 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
val get_depth : config -> int
0 means prover default

Results


type verdict = 
| NoResult
| Invalid
| Unknown
| Timeout
| Stepout
| Computing of (unit -> unit)
| Checked
| Valid
| Failed
type result = {
   verdict : verdict;
   solver_time : float;
   prover_time : float;
   prover_steps : int;
   prover_depth : 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 : 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 result : ?solver:float ->
?time:float -> ?steps:int -> ?depth:int -> verdict -> result
val is_auto : prover -> bool
val is_verdict : result -> bool
val is_valid : 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 dkey_no_time_info : Log.category
val dkey_no_step_info : Log.category
val dkey_no_goals_info : Log.category