From 7fe487b6af143b85d54aa41fd395ca3075e3e629 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 8 Jul 2022 17:53:07 +0200
Subject: [PATCH] [wp] fix prover title
---
src/plugins/wp/Stats.ml | 3 ++-
src/plugins/wp/VCS.ml | 7 +++++--
src/plugins/wp/VCS.mli | 2 +-
3 files changed, 8 insertions(+), 4 deletions(-)
diff --git a/src/plugins/wp/Stats.ml b/src/plugins/wp/Stats.ml
index b175e95b7c7..de3d5cee53e 100644
--- a/src/plugins/wp/Stats.ml
+++ b/src/plugins/wp/Stats.ml
@@ -207,7 +207,8 @@ let pp_stats fmt s =
List.iter
(fun (p,pr) ->
let success = truncate pr.success in
- Format.fprintf fmt " (%a" VCS.pp_prover p ;
+ let title = VCS.title_of_prover ~version:false p in
+ Format.fprintf fmt " (%s" title ;
if success > 0 && np > 1 then
Format.fprintf fmt " %d/%d" success np ;
if not shell && pr.time > Rformat.epsilon then
diff --git a/src/plugins/wp/VCS.ml b/src/plugins/wp/VCS.ml
index 8ed3c20de0e..a280067c96a 100644
--- a/src/plugins/wp/VCS.ml
+++ b/src/plugins/wp/VCS.ml
@@ -79,9 +79,12 @@ let name_of_prover = function
| Qed -> "qed"
| Tactical -> "script"
-let title_of_prover = function
+let title_of_prover ?version = function
| Why3 s ->
- if Wp_parameters.has_dkey dkey_shell
+ let v = match version with Some v -> v | None ->
+ Wp_parameters.has_dkey dkey_shell
+ in
+ if v
then Why3Provers.name s
else Why3Provers.title s
| Qed -> "Qed"
diff --git a/src/plugins/wp/VCS.mli b/src/plugins/wp/VCS.mli
index e4dc8bac052..d1b89ddddd8 100644
--- a/src/plugins/wp/VCS.mli
+++ b/src/plugins/wp/VCS.mli
@@ -42,7 +42,7 @@ 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 title_of_prover : ?version:bool -> prover -> string
val filename_for_prover : prover -> string
val title_of_mode : mode -> string
--
GitLab