From b4b2971e67eb83c688ed9b5b364f795059327e2b Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 16 Jun 2020 11:59:12 +0200
Subject: [PATCH] [wp] Removed debug-keys, use shell - removed no-time-info -
removed no-step-info - removed no-goals-info - removed no-cache-info -
removed success-only
---
src/plugins/wp/VCS.ml | 17 ++--
src/plugins/wp/VCS.mli | 5 --
src/plugins/wp/register.ml | 85 +++++++++----------
src/plugins/wp/tests/README.md | 2 +-
src/plugins/wp/tests/test_config_qualif | 2 +-
src/plugins/wp/tests/wp/stmtcompiler_test.i | 2 +-
.../wp/tests/wp/stmtcompiler_test_rela.i | 2 +-
src/plugins/wp/tests/wp/wp_strategy.c | 4 +-
src/plugins/wp/tests/wp_acsl/boolean.i | 2 +-
.../wp_acsl/oracle_qualif/cnf.res.oracle | 2 +-
.../oracle/frama_c_hashtbl_solved.res.oracle | 1 -
.../frama_c_hashtbl_solved.res.oracle | 1 -
src/plugins/wp/tests/wp_manual/manual.i | 6 +-
.../oracle_qualif/removed.res.oracle | 5 +-
.../wp/tests/wp_plugin/oracle_qualif/stmt.log | 1 +
src/plugins/wp/tests/wp_plugin/removed.i | 2 +-
src/plugins/wp/tests/wp_plugin/stmt.c | 2 +-
.../wp_typed/oracle/user_init.0.res.oracle | 1 -
.../wp_typed/oracle/user_init.1.res.oracle | 1 -
src/plugins/wp/wpo.ml | 2 +-
20 files changed, 64 insertions(+), 81 deletions(-)
diff --git a/src/plugins/wp/VCS.ml b/src/plugins/wp/VCS.ml
index 0cf379c647a..c92b0ca59fb 100644
--- a/src/plugins/wp/VCS.ml
+++ b/src/plugins/wp/VCS.ml
@@ -25,11 +25,6 @@
(* -------------------------------------------------------------------------- *)
let dkey_shell = Wp_parameters.register_category "shell"
-let dkey_no_time_info = Wp_parameters.register_category "no-time-info"
-let dkey_no_step_info = Wp_parameters.register_category "no-step-info"
-let dkey_no_goals_info = Wp_parameters.register_category "no-goals-info"
-let dkey_no_cache_info = Wp_parameters.register_category "no-cache-info"
-let dkey_success_only = Wp_parameters.register_category "success-only"
type prover =
| Why3 of Why3Provers.t (* Prover via WHY *)
@@ -92,7 +87,7 @@ let name_of_prover = function
let title_of_prover = function
| Why3 s ->
- if Wp_parameters.has_dkey dkey_success_only
+ if Wp_parameters.has_dkey dkey_shell
then Why3Provers.name s
else Why3Provers.title s
| NativeAltErgo -> "Alt-Ergo (native)"
@@ -299,15 +294,15 @@ let perfo dkey = not (Wp_parameters.has_dkey dkey)
let pp_perf fmt r =
begin
let t = r.solver_time in
- if t > Rformat.epsilon && perfo dkey_no_time_info
+ if t > Rformat.epsilon && perfo dkey_shell
then Format.fprintf fmt " (Qed:%a)" Rformat.pp_time t ;
let t = r.prover_time in
- if t > Rformat.epsilon && perfo dkey_no_time_info
+ if t > Rformat.epsilon && perfo dkey_shell
then Format.fprintf fmt " (%a)" Rformat.pp_time t ;
let s = r.prover_steps in
- if s > 0 && perfo dkey_no_step_info
+ if s > 0 && perfo dkey_shell
then Format.fprintf fmt " (%d)" s ;
- if r.cached && perfo dkey_no_cache_info
+ if r.cached && perfo dkey_shell
then Format.fprintf fmt " (cached)" ;
end
@@ -335,7 +330,7 @@ let pp_cache_miss fmt st prover r =
Format.pp_print_string fmt (if is_valid r then "Valid" else "Unsuccess")
let pp_result_qualif prover fmt r =
- if Wp_parameters.has_dkey dkey_success_only then
+ if Wp_parameters.has_dkey dkey_shell then
match r.verdict with
| NoResult -> Format.pp_print_string fmt "No Result"
| Computing _ -> Format.pp_print_string fmt "Computing"
diff --git a/src/plugins/wp/VCS.mli b/src/plugins/wp/VCS.mli
index 3e1acbf04bb..0e869ebea14 100644
--- a/src/plugins/wp/VCS.mli
+++ b/src/plugins/wp/VCS.mli
@@ -127,8 +127,3 @@ val choose : result -> result -> result
val best : result list -> result
val dkey_shell: Wp_parameters.category
-val dkey_no_time_info: Wp_parameters.category
-val dkey_no_step_info: Wp_parameters.category
-val dkey_no_goals_info: Wp_parameters.category
-val dkey_no_cache_info: Wp_parameters.category
-val dkey_success_only: Wp_parameters.category
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index 2a0acd067fa..c350f0f5779 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -263,20 +263,17 @@ let add_time s t =
end
let do_list_scheduled iter_on_goals =
- if not (Wp_parameters.has_dkey VCS.dkey_no_goals_info) then
- begin
- clear_scheduled () ;
- iter_on_goals
- (fun goal ->
- begin
- incr scheduled ;
- if !spy then session := GOALS.add goal !session ;
- end) ;
- match !scheduled with
- | 0 -> Wp_parameters.warning ~current:false "No goal generated"
- | 1 -> Wp_parameters.feedback "1 goal scheduled"
- | n -> Wp_parameters.feedback "%d goals scheduled" n
- end
+ clear_scheduled () ;
+ iter_on_goals
+ (fun goal ->
+ begin
+ incr scheduled ;
+ if !spy then session := GOALS.add goal !session ;
+ end) ;
+ match !scheduled with
+ | 0 -> Wp_parameters.warning ~current:false "No goal generated"
+ | 1 -> Wp_parameters.feedback "1 goal scheduled"
+ | n -> Wp_parameters.feedback "%d goals scheduled" n
let dkey_prover = Wp_parameters.register_category "prover"
@@ -305,8 +302,7 @@ let do_progress goal msg =
let do_report_cache_usage mode =
if !exercised > 0 &&
- not (Wp_parameters.has_dkey VCS.dkey_shell) &&
- not (Wp_parameters.has_dkey VCS.dkey_no_cache_info)
+ not (Wp_parameters.has_dkey VCS.dkey_shell)
then
let hits = Cache.get_hits () in
let miss = Cache.get_miss () in
@@ -450,8 +446,7 @@ let do_report_time fmt s =
begin
if s.n_time > 0 &&
s.u_time > Rformat.epsilon &&
- not (Wp_parameters.has_dkey VCS.dkey_no_time_info) &&
- not (Wp_parameters.has_dkey VCS.dkey_success_only)
+ not (Wp_parameters.has_dkey VCS.dkey_shell)
then
let mean = s.a_time /. float s.n_time in
let epsilon = 0.05 *. mean in
@@ -474,14 +469,13 @@ let do_report_time fmt s =
let do_report_steps fmt s =
begin
if s.steps > 0 &&
- not (Wp_parameters.has_dkey VCS.dkey_no_step_info) &&
- not (Wp_parameters.has_dkey VCS.dkey_success_only)
+ not (Wp_parameters.has_dkey VCS.dkey_shell)
then
Format.fprintf fmt " (%d)" s.steps ;
end
let do_report_stopped fmt s =
- if Wp_parameters.has_dkey VCS.dkey_success_only then
+ if Wp_parameters.has_dkey VCS.dkey_shell then
begin
let n = s.interrupted + s.unknown in
if n > 0 then
@@ -510,27 +504,26 @@ let do_report_prover_stats pp_prover fmt (p,s) =
end
let do_report_scheduled () =
- if not (Wp_parameters.has_dkey VCS.dkey_no_goals_info) then
- if Wp_parameters.Generate.get () then
- let plural = if !exercised > 1 then "s" else "" in
- Wp_parameters.result "%d goal%s generated" !exercised plural
- else
- if !scheduled > 0 then
- begin
- let proved = GOALS.cardinal !proved in
- let mode = Cache.get_mode () in
- if mode <> Cache.NoCache then do_report_cache_usage mode ;
- Wp_parameters.result "%t"
- begin fun fmt ->
- Format.fprintf fmt "Proved goals: %4d / %d@\n" proved !scheduled ;
- Pretty_utils.pp_items
- ~min:12 ~align:`Left
- ~title:(fun (prover,_) -> VCS.title_of_prover prover)
- ~iter:(fun f -> PM.iter (fun p s -> f (p,s)) !provers)
- ~pp_title:(fun fmt a -> Format.fprintf fmt "%s:" a)
- ~pp_item:do_report_prover_stats fmt ;
- end ;
- end
+ if Wp_parameters.Generate.get () then
+ let plural = if !exercised > 1 then "s" else "" in
+ Wp_parameters.result "%d goal%s generated" !exercised plural
+ else
+ if !scheduled > 0 then
+ begin
+ let proved = GOALS.cardinal !proved in
+ let mode = Cache.get_mode () in
+ if mode <> Cache.NoCache then do_report_cache_usage mode ;
+ Wp_parameters.result "%t"
+ begin fun fmt ->
+ Format.fprintf fmt "Proved goals: %4d / %d@\n" proved !scheduled ;
+ Pretty_utils.pp_items
+ ~min:12 ~align:`Left
+ ~title:(fun (prover,_) -> VCS.title_of_prover prover)
+ ~iter:(fun f -> PM.iter (fun p s -> f (p,s)) !provers)
+ ~pp_title:(fun fmt a -> Format.fprintf fmt "%s:" a)
+ ~pp_item:do_report_prover_stats fmt ;
+ end ;
+ end
let do_list_scheduled_result () =
begin
@@ -738,8 +731,7 @@ let do_cache_cleanup () =
Cache.cleanup_cache () ;
let removed = Cache.get_removed () in
if removed > 0 &&
- not (Wp_parameters.has_dkey VCS.dkey_shell) &&
- not (Wp_parameters.has_dkey VCS.dkey_no_cache_info)
+ not (Wp_parameters.has_dkey VCS.dkey_shell)
then
Wp_parameters.result "[Cache] removed:%d" removed
end
@@ -905,7 +897,10 @@ let pp_wp_parameters fmt =
if Wp_parameters.RTE.get () then Format.pp_print_string fmt " -wp-rte" ;
let spec = Wp_parameters.Model.get () in
if spec <> [] && spec <> ["Typed"] then
- ( let descr = Factory.descr (Factory.parse spec) in
+ ( let descr =
+ if spec = ["Dump"] then "Dump"
+ else Factory.descr (Factory.parse spec)
+ in
Format.fprintf fmt " -wp-model '%s'" descr ) ;
if not (Wp_parameters.Let.get ()) then Format.pp_print_string fmt
" -wp-no-let" ;
diff --git a/src/plugins/wp/tests/README.md b/src/plugins/wp/tests/README.md
index 2eb7d3d587b..181dab0d59b 100644
--- a/src/plugins/wp/tests/README.md
+++ b/src/plugins/wp/tests/README.md
@@ -63,7 +63,7 @@ below for details.
To be accepted by Frama-CI, tests in « qualif » configuration must be easily
reproducible on any platform. This is checked by running WP with flag
-`-wp-msg-key success-only` which is set by the default in the qualif test
+`-wp-msg-key shell` which is set by the default in the qualif test
configuration. Hence, a qualified test result only contains proof status that
are either:
- failed
diff --git a/src/plugins/wp/tests/test_config_qualif b/src/plugins/wp/tests/test_config_qualif
index 29195ff38b1..82ac2379722 100644
--- a/src/plugins/wp/tests/test_config_qualif
+++ b/src/plugins/wp/tests/test_config_qualif
@@ -1,2 +1,2 @@
-CMD: @frama-c@ -no-autoload-plugins -load-module wp -wp -wp-par 1 -wp-share ./share -wp-msg-key shell,success-only -wp-report tests/qualif.report -wp-session @PTEST_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.session -wp-cache-env -wp-cache replay @PTEST_FILE@ -wp-coq-timeout 120
+CMD: @frama-c@ -no-autoload-plugins -load-module wp -wp -wp-par 1 -wp-share ./share -wp-msg-key shell -wp-report tests/qualif.report -wp-session @PTEST_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.session -wp-cache-env -wp-cache replay @PTEST_FILE@ -wp-coq-timeout 120
OPT:
diff --git a/src/plugins/wp/tests/wp/stmtcompiler_test.i b/src/plugins/wp/tests/wp/stmtcompiler_test.i
index 264b9e58d48..c610d545492 100644
--- a/src/plugins/wp/tests/wp/stmtcompiler_test.i
+++ b/src/plugins/wp/tests/wp/stmtcompiler_test.i
@@ -1,5 +1,5 @@
/* run.config
- OPT: -load-script tests/wp/stmtcompiler_test.ml -wp-msg-key success-only
+ OPT: -load-script tests/wp/stmtcompiler_test.ml -wp-msg-key shell
*/
int empty (int c){
diff --git a/src/plugins/wp/tests/wp/stmtcompiler_test_rela.i b/src/plugins/wp/tests/wp/stmtcompiler_test_rela.i
index 4dafe25db11..b206efad051 100644
--- a/src/plugins/wp/tests/wp/stmtcompiler_test_rela.i
+++ b/src/plugins/wp/tests/wp/stmtcompiler_test_rela.i
@@ -1,5 +1,5 @@
/* run.config_qualif
- OPT: -load-script tests/wp/stmtcompiler_test_rela.ml -wp-msg-key success-only
+ OPT: -load-script tests/wp/stmtcompiler_test_rela.ml -wp-msg-key shell
*/
int empty (int c){
diff --git a/src/plugins/wp/tests/wp/wp_strategy.c b/src/plugins/wp/tests/wp/wp_strategy.c
index 0afd35c1320..c514347a72a 100644
--- a/src/plugins/wp/tests/wp/wp_strategy.c
+++ b/src/plugins/wp/tests/wp/wp_strategy.c
@@ -4,7 +4,7 @@ OPT: -journal-disable -wp-model Typed -wp-verbose 2 -wp-prop @assigns
*/
/* run.config_qualif
-OPT: -journal-disable -rte -wp -wp-model Hoare -wp-par 1 -wp-msg-key "success-only"
+OPT: -journal-disable -rte -wp -wp-model Hoare -wp-par 1 -wp-msg-key shell
*/
/*----------------------------------------------------------------------------*/
@@ -89,7 +89,7 @@ int default_behaviors (int c, int x) {
int y;
//@ ensures qed_ok: stmt_p: x > 0; assigns qed_ok: x;
- if (c) x = 1;
+ if (c) x = 1;
else {
//@ assert qed_ok: x >= 0;
x++;
diff --git a/src/plugins/wp/tests/wp_acsl/boolean.i b/src/plugins/wp/tests/wp_acsl/boolean.i
index f8e7f458b4f..79f94c24a8a 100644
--- a/src/plugins/wp/tests/wp_acsl/boolean.i
+++ b/src/plugins/wp/tests/wp_acsl/boolean.i
@@ -1,5 +1,5 @@
/* run.config
-OPT: -wp-gen -wp-prover why3 -wp-msg-key success-only
+OPT: -wp-gen -wp-prover why3 -wp-msg-key shell
*/
/*@
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/cnf.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/cnf.res.oracle
index 40c0c6de692..979b8b88f24 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/cnf.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/cnf.res.oracle
@@ -305,4 +305,4 @@
Functions WP Alt-Ergo Total Success
f 12 31 43 100%
------------------------------------------------------------
-[wp] Logging keys: success-only,shell,cnf.
+[wp] Logging keys: shell,cnf.
diff --git a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_hashtbl_solved.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_hashtbl_solved.res.oracle
index 00a8df49e16..064dce264b9 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_hashtbl_solved.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_hashtbl_solved.res.oracle
@@ -8,7 +8,6 @@
[rte] annotating function init
[rte] annotating function mem_binding
[rte] annotating function size
-[wp] Computing [100 goals...]
[wp] Goal typed_add_complete_full_nominal : not tried
[wp] Goal typed_add_disjoint_full_nominal : not tried
[wp] Goal typed_add_assert_rte_index_bound : not tried
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle
index 6e3fc54c35c..8e5320587c9 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle
@@ -3,7 +3,6 @@
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
-[wp] Computing [100 goals...]
[wp] 102 goals scheduled
[wp] [Alt-Ergo] Goal typed_add_complete_full_nominal : Valid
[wp] [Alt-Ergo] Goal typed_add_disjoint_full_nominal : Valid
diff --git a/src/plugins/wp/tests/wp_manual/manual.i b/src/plugins/wp/tests/wp_manual/manual.i
index 7cd72107d4c..11a04e0783a 100644
--- a/src/plugins/wp/tests/wp_manual/manual.i
+++ b/src/plugins/wp/tests/wp_manual/manual.i
@@ -2,8 +2,8 @@
DONTRUN:
*/
/* run.config_qualif
- OPT: -wp-msg-key no-time-info @PTEST_DIR@/working_dir/swap.c @PTEST_DIR@/working_dir/swap1.h
- OPT: -wp-msg-key no-time-info -wp-rte @PTEST_DIR@/working_dir/swap.c @PTEST_DIR@/working_dir/swap2.h
- OPT: -load-module report -kernel-verbose 0 -wp-msg-key no-time-info -wp-rte @PTEST_DIR@/working_dir/swap.c @PTEST_DIR@/working_dir/swap2.h -wp-verbose 0 -then -no-unicode -report
+ OPT: -wp-msg-key shell @PTEST_DIR@/working_dir/swap.c @PTEST_DIR@/working_dir/swap1.h
+ OPT: -wp-msg-key shell -wp-rte @PTEST_DIR@/working_dir/swap.c @PTEST_DIR@/working_dir/swap2.h
+ OPT: -load-module report -kernel-verbose 0 -wp-msg-key shell -wp-rte @PTEST_DIR@/working_dir/swap.c @PTEST_DIR@/working_dir/swap2.h -wp-verbose 0 -then -no-unicode -report
*/
void look_at_working_dir(void);
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/removed.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/removed.res.oracle
index 98b421111a0..0e98bda081d 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/removed.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/removed.res.oracle
@@ -1,10 +1,11 @@
+# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/removed.i (no preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-
-[eva:alarm] tests/wp_plugin/removed.i:10: Warning:
+
+[eva:alarm] tests/wp_plugin/removed.i:10: Warning:
signed overflow. assert 1 + i ≤ 2147483647;
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.log b/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.log
index efc57b6183b..583f4d36f08 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.log
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.log
@@ -1,3 +1,4 @@
+# frama-c -wp -wp-model 'Dump' [...]
[kernel] Parsing tests/wp_plugin/stmt.c (with preprocessing)
[wp] Running WP plugin...
[wp] [CFG] Goal f_exits : Valid (Unreachable)
diff --git a/src/plugins/wp/tests/wp_plugin/removed.i b/src/plugins/wp/tests/wp_plugin/removed.i
index f27fb0df1d6..a0e4b8e3fef 100644
--- a/src/plugins/wp/tests/wp_plugin/removed.i
+++ b/src/plugins/wp/tests/wp_plugin/removed.i
@@ -1,5 +1,5 @@
/* run.config_qualif
- CMD: @frama-c@ -wp-share ./share -wp-msg-key no-cache-info,success-only -wp-par 1 -wp-session @PTEST_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.session -wp-cache replay -wp-cache-dir ./cache
+ CMD: @frama-c@ -wp-share ./share -wp-msg-key shell -wp-par 1 -wp-session @PTEST_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.session -wp-cache replay -wp-cache-dir ./cache
OPT: -eva -eva-msg-key=-summary -then -wp -then -no-eva -warn-unsigned-overflow -wp
*/
diff --git a/src/plugins/wp/tests/wp_plugin/stmt.c b/src/plugins/wp/tests/wp_plugin/stmt.c
index 02e1eddff38..58e04b9d85f 100644
--- a/src/plugins/wp/tests/wp_plugin/stmt.c
+++ b/src/plugins/wp/tests/wp_plugin/stmt.c
@@ -4,7 +4,7 @@
/* run.config_qualif
OPT: -load-module report -then -report
- EXECNOW: LOG stmt.log LOG f.dot LOG f_default_for_stmt_2.dot LOG g.dot LOG g_default_for_stmt_11.dot @frama-c@ -no-autoload-plugins -load-module wp -wp-precond-weakening -wp -wp-model Dump -wp-out tests/wp_plugin/result_qualif -wp-msg-key no-cache-info @PTEST_FILE@ 1> tests/wp_plugin/result_qualif/stmt.log
+ EXECNOW: LOG stmt.log LOG f.dot LOG f_default_for_stmt_2.dot LOG g.dot LOG g_default_for_stmt_11.dot @frama-c@ -no-autoload-plugins -load-module wp -wp-precond-weakening -wp -wp-model Dump -wp-out tests/wp_plugin/result_qualif -wp-msg-key shell @PTEST_FILE@ 1> tests/wp_plugin/result_qualif/stmt.log
*/
/*@ ensures a > 0 ==> \result == a + b;
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle
index 999fd9b7424..e8e6e13bc58 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle
@@ -8,7 +8,6 @@
[wp] [CFG] Goal init_t2_v2_exits : Valid (Unreachable)
[wp] [CFG] Goal init_t2_v3_exits : Valid (Unreachable)
[wp] Warning: Missing RTE guards
-[wp] Computing [100 goals...]
------------------------------------------------------------
Function init
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle
index e6996907f93..aa1fcfbc2ff 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle
@@ -8,7 +8,6 @@
[wp] [CFG] Goal init_t2_v2_exits : Valid (Unreachable)
[wp] [CFG] Goal init_t2_v3_exits : Valid (Unreachable)
[wp] Warning: Missing RTE guards
-[wp] Computing [100 goals...]
------------------------------------------------------------
Function init
------------------------------------------------------------
diff --git a/src/plugins/wp/wpo.ml b/src/plugins/wp/wpo.ml
index 4f85fe8851b..1d6649a3de7 100644
--- a/src/plugins/wp/wpo.ml
+++ b/src/plugins/wp/wpo.ml
@@ -659,7 +659,7 @@ let add g =
Gmap.iter
(fun _ ws -> WPOset.iter (fun _ -> incr added) ws)
system.wpo_idx ;
- if not (Wp_parameters.has_dkey VCS.dkey_no_goals_info) then
+ if not (Wp_parameters.has_dkey VCS.dkey_shell) then
Wp_parameters.feedback ~ontty:`Feedback "Computing [%d goals...]" !added ;
added := 0 ;
end ;
--
GitLab