From eee9a6a93f42df577ca444ca4761632b5fa05c76 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr> Date: Mon, 2 Mar 2020 16:54:31 +0100 Subject: [PATCH] [wp] hide prover versions in qualif tests --- src/plugins/wp/VCS.ml | 13 +++++-------- src/plugins/wp/Why3Provers.ml | 1 + src/plugins/wp/Why3Provers.mli | 1 + 3 files changed, 7 insertions(+), 8 deletions(-) diff --git a/src/plugins/wp/VCS.ml b/src/plugins/wp/VCS.ml index 0479e18eca4..456c225e275 100644 --- a/src/plugins/wp/VCS.ml +++ b/src/plugins/wp/VCS.ml @@ -90,7 +90,10 @@ let name_of_prover = function | Tactical -> "script" let title_of_prover = function - | Why3 s -> Why3Provers.title s + | Why3 s -> + if Wp_parameters.has_dkey dkey_success_only + then Why3Provers.name s + else Why3Provers.title s | NativeAltErgo -> "Alt-Ergo (native)" | NativeCoq -> "Coq (native)" | Qed -> "Qed" @@ -142,13 +145,7 @@ let cmp_prover p q = | _ , NativeCoq -> 1 | Why3 p , Why3 q -> Why3Provers.compare p q -let pp_prover fmt = function - | NativeAltErgo -> Format.pp_print_string fmt "Alt-Ergo (Native)" - | NativeCoq -> Format.pp_print_string fmt "Coq (Native)" - | Why3 smt -> Format.pp_print_string fmt (Why3Provers.title smt) - | Qed -> Format.fprintf fmt "Qed" - | Tactical -> Format.pp_print_string fmt "Tactical" - +let pp_prover fmt p = Format.pp_print_string fmt (title_of_prover p) let pp_mode fmt m = Format.pp_print_string fmt (title_of_mode m) module P = struct type t = prover let compare = cmp_prover end diff --git a/src/plugins/wp/Why3Provers.ml b/src/plugins/wp/Why3Provers.ml index 7c7095340b0..aa52b12ef95 100644 --- a/src/plugins/wp/Why3Provers.ml +++ b/src/plugins/wp/Why3Provers.ml @@ -92,6 +92,7 @@ let print_wp s = String.concat ":" prv let title p = Pretty_utils.sfprintf "%a" Why3.Whyconf.print_prover p +let name p = p.Why3.Whyconf.prover_name let compare = Why3.Whyconf.Prover.compare let provers () = diff --git a/src/plugins/wp/Why3Provers.mli b/src/plugins/wp/Why3Provers.mli index 2e53fcdbead..43e65783484 100644 --- a/src/plugins/wp/Why3Provers.mli +++ b/src/plugins/wp/Why3Provers.mli @@ -35,6 +35,7 @@ val find_fallback : string -> fallback val print_why3 : t -> string val print_wp : t -> string val title : t -> string +val name : t -> string val compare : t -> t -> int val provers : unit -> t list -- GitLab