Wp.VCS
Provers and Proof Obligations Results
Verification Condition Status
type prover =
| Why3 of Why3Provers.t
Prover via WHY
*)| Qed
Qed Solver
*)| Tactical
Interactive Prover
*)val provers : unit -> prover list
Mainstream installed provers
val name_of_prover : prover -> string
val title_of_prover : ?version:bool -> 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
None
means current WP option default. Some 0
means prover default.
val current : unit -> config
Current parameters
val default : config
all None
val get_timeout :
?kf:Frama_c_kernel.Kernel_function.t ->
smoke:bool ->
config ->
float
0.0 means no-timeout
val get_stepout : config -> int
0 means no-stepout
val get_memlimit : config -> int
0 means no-memlimit
type result = {
verdict : verdict;
cached : bool;
solver_time : float;
prover_time : float;
prover_steps : int;
prover_errpos : Stdlib.Lexing.position option;
prover_errmsg : string;
}
val no_result : result
val valid : result
val unknown : result
val stepout : int -> result
val timeout : float -> 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 is_auto : prover -> bool
val is_result : verdict -> bool
val is_verdict : result -> bool
val is_valid : result -> bool
val is_trivial : result -> bool
val is_not_valid : result -> bool
val is_computing : result -> bool
val is_proved : smoke:bool -> verdict -> bool
val autofit : result -> bool
Result that fits the default configuration
val name_of_verdict : verdict -> string
val pp_result : Stdlib.Format.formatter -> result -> unit
val dkey_shell : Wp_parameters.category