Module Wp.VCS

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