From c635c8181de3a798539703956d268b4b7a7fa5e0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 20 Feb 2020 11:19:16 +0100
Subject: [PATCH] [wp] emit a warning when no generated goal
---
src/plugins/wp/Changelog | 1 +
src/plugins/wp/register.ml | 37 ++++++++++---------
.../wp_plugin/oracle_qualif/nowp.res.oracle | 3 +-
.../oracle_qualif/removed.res.oracle | 3 +-
.../oracle_qualif/sequence.2.res.oracle | 3 +-
.../wp/tests/wp_plugin/oracle_qualif/stmt.log | 3 +-
.../wp_region/oracle_qualif/array1.res.oracle | 3 +-
.../wp_region/oracle_qualif/array2.res.oracle | 3 +-
.../wp_region/oracle_qualif/array3.res.oracle | 3 +-
.../wp_region/oracle_qualif/array4.res.oracle | 3 +-
.../wp_region/oracle_qualif/array5.res.oracle | 3 +-
.../wp_region/oracle_qualif/array6.res.oracle | 3 +-
.../wp_region/oracle_qualif/array7.res.oracle | 3 +-
.../wp_region/oracle_qualif/array8.res.oracle | 3 +-
.../wp_region/oracle_qualif/fb_ADD.res.oracle | 3 +-
.../oracle_qualif/fb_SORT.res.oracle | 3 +-
.../oracle_qualif/garbled.res.oracle | 3 +-
.../wp_region/oracle_qualif/index.res.oracle | 3 +-
.../wp_region/oracle_qualif/matrix.res.oracle | 3 +-
.../oracle_qualif/structarray1.res.oracle | 3 +-
.../oracle_qualif/structarray2.res.oracle | 3 +-
.../oracle_qualif/structarray3.res.oracle | 3 +-
.../oracle_qualif/structarray4.res.oracle | 3 +-
.../wp_region/oracle_qualif/swap.res.oracle | 3 +-
24 files changed, 43 insertions(+), 61 deletions(-)
diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index e2b37ee75a6..4e411b02187 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -25,6 +25,7 @@
- WP [2020/02/10] Extended frame conditions with global C-types
- WP [2019/17/04] Control splitting with -wp-max-split <n>
- WP [2019/12/04] Added option -wp-run-all-provers
+- WP [2019/01/29] Emit a warning when no goal is generated
##########################
Plugin WP 20.0 (Calcium)
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index 5ee0a232c14..cc4ced4bfa6 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -272,10 +272,10 @@ let do_list_scheduled iter_on_goals =
incr scheduled ;
if !spy then session := GOALS.add goal !session ;
end) ;
- let n = !scheduled in
- if n > 1
- then Wp_parameters.feedback "%d goals scheduled" n
- else Wp_parameters.feedback "%d goal scheduled" n ;
+ 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
let dkey_prover = Wp_parameters.register_category "prover"
@@ -487,19 +487,22 @@ let do_report_scheduled () =
let plural = if !exercised > 1 then "s" else "" in
Wp_parameters.result "%d goal%s generated" !exercised plural
else
- let proved = GOALS.cardinal !proved in
- let mode = ProverWhy3.get_mode () in
- if mode <> ProverWhy3.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
+ if !scheduled > 0 then
+ begin
+ let proved = GOALS.cardinal !proved in
+ let mode = ProverWhy3.get_mode () in
+ if mode <> ProverWhy3.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
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nowp.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nowp.res.oracle
index a3a203eb6c7..28d3b1aac61 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nowp.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nowp.res.oracle
@@ -3,6 +3,5 @@
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
-[wp] 0 goal scheduled
-[wp] Proved goals: 0 / 0
+[wp] Warning: No goal generated
------------------------------------------------------------
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 6d0cc9b254a..f231fb042cb 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
@@ -18,5 +18,4 @@
[wp] Proved goals: 0 / 1
Alt-Ergo 2.0.0: 0 (unsuccess: 1)
[wp] Running WP plugin...
-[wp] 0 goal scheduled
-[wp] Proved goals: 0 / 0
+[wp] Warning: No goal generated
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.2.res.oracle
index 2e0c8f96387..b58e86cce5e 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.2.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.2.res.oracle
@@ -3,6 +3,5 @@
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
-[wp] 0 goal scheduled
-[wp] Proved goals: 0 / 0
+[wp] Warning: No goal generated
------------------------------------------------------------
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 a4c56847582..efc57b6183b 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.log
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.log
@@ -17,5 +17,4 @@
[wp] CFG g -> g_default_for_stmt_11
[wp] CFG f -> f
[wp] CFG f -> f_default_for_stmt_2
-[wp] 0 goal scheduled
-[wp] Proved goals: 0 / 0
+[wp] Warning: No goal generated
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/array1.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/array1.res.oracle
index 00091d72a9f..ed869315385 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/array1.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/array1.res.oracle
@@ -3,6 +3,5 @@
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
-[wp] 0 goal scheduled
-[wp] Proved goals: 0 / 0
+[wp] Warning: No goal generated
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/array2.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/array2.res.oracle
index 256b9a73626..5e7de78ee60 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/array2.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/array2.res.oracle
@@ -3,6 +3,5 @@
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
-[wp] 0 goal scheduled
-[wp] Proved goals: 0 / 0
+[wp] Warning: No goal generated
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/array3.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/array3.res.oracle
index 2ead4dbe67b..d46d52bdc2c 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/array3.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/array3.res.oracle
@@ -3,6 +3,5 @@
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
-[wp] 0 goal scheduled
-[wp] Proved goals: 0 / 0
+[wp] Warning: No goal generated
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/array4.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/array4.res.oracle
index 03f4311ee37..b732e6a34d5 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/array4.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/array4.res.oracle
@@ -3,6 +3,5 @@
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
-[wp] 0 goal scheduled
-[wp] Proved goals: 0 / 0
+[wp] Warning: No goal generated
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/array5.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/array5.res.oracle
index c106bd36a02..31f6983483f 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/array5.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/array5.res.oracle
@@ -3,6 +3,5 @@
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
-[wp] 0 goal scheduled
-[wp] Proved goals: 0 / 0
+[wp] Warning: No goal generated
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/array6.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/array6.res.oracle
index d582428d468..34d7eb2a982 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/array6.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/array6.res.oracle
@@ -3,6 +3,5 @@
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
-[wp] 0 goal scheduled
-[wp] Proved goals: 0 / 0
+[wp] Warning: No goal generated
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/array7.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/array7.res.oracle
index 0eb3a6468cf..0e0ad91c163 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/array7.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/array7.res.oracle
@@ -3,6 +3,5 @@
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
-[wp] 0 goal scheduled
-[wp] Proved goals: 0 / 0
+[wp] Warning: No goal generated
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/array8.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/array8.res.oracle
index 9ea4ec380db..13c02c6b2d1 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/array8.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/array8.res.oracle
@@ -3,6 +3,5 @@
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
-[wp] 0 goal scheduled
-[wp] Proved goals: 0 / 0
+[wp] Warning: No goal generated
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/fb_ADD.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/fb_ADD.res.oracle
index 67c1fd0139e..0db49291906 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/fb_ADD.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/fb_ADD.res.oracle
@@ -3,6 +3,5 @@
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
-[wp] 0 goal scheduled
-[wp] Proved goals: 0 / 0
+[wp] Warning: No goal generated
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/fb_SORT.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/fb_SORT.res.oracle
index 03dd7d0a795..372e798b673 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/fb_SORT.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/fb_SORT.res.oracle
@@ -3,6 +3,5 @@
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
-[wp] 0 goal scheduled
-[wp] Proved goals: 0 / 0
+[wp] Warning: No goal generated
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/garbled.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/garbled.res.oracle
index 47692e24e29..af0aea662d2 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/garbled.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/garbled.res.oracle
@@ -3,6 +3,5 @@
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
-[wp] 0 goal scheduled
-[wp] Proved goals: 0 / 0
+[wp] Warning: No goal generated
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/index.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/index.res.oracle
index 2a4bfbb4975..fe16dc545ec 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/index.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/index.res.oracle
@@ -3,6 +3,5 @@
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
-[wp] 0 goal scheduled
-[wp] Proved goals: 0 / 0
+[wp] Warning: No goal generated
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/matrix.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/matrix.res.oracle
index a17c2fcf344..d0a1dcf567a 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/matrix.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/matrix.res.oracle
@@ -3,6 +3,5 @@
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
-[wp] 0 goal scheduled
-[wp] Proved goals: 0 / 0
+[wp] Warning: No goal generated
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/structarray1.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/structarray1.res.oracle
index 3917685de3c..4f31df7dff8 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/structarray1.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/structarray1.res.oracle
@@ -3,6 +3,5 @@
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
-[wp] 0 goal scheduled
-[wp] Proved goals: 0 / 0
+[wp] Warning: No goal generated
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/structarray2.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/structarray2.res.oracle
index 8360b587599..94c1cbf1865 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/structarray2.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/structarray2.res.oracle
@@ -3,6 +3,5 @@
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
-[wp] 0 goal scheduled
-[wp] Proved goals: 0 / 0
+[wp] Warning: No goal generated
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/structarray3.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/structarray3.res.oracle
index e317fb0d4fd..0cee2a2b631 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/structarray3.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/structarray3.res.oracle
@@ -3,6 +3,5 @@
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
-[wp] 0 goal scheduled
-[wp] Proved goals: 0 / 0
+[wp] Warning: No goal generated
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/structarray4.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/structarray4.res.oracle
index e1a7716376a..70c1d992d17 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/structarray4.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/structarray4.res.oracle
@@ -3,6 +3,5 @@
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
-[wp] 0 goal scheduled
-[wp] Proved goals: 0 / 0
+[wp] Warning: No goal generated
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/swap.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/swap.res.oracle
index a41a5ede9f8..258e09a4a69 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/swap.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/swap.res.oracle
@@ -3,6 +3,5 @@
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
-[wp] 0 goal scheduled
-[wp] Proved goals: 0 / 0
+[wp] Warning: No goal generated
------------------------------------------------------------
--
GitLab