diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index e2b37ee75a62b79ec404911fc5f8ad843a2968d9..4e411b021875f01b7c949d36ca11740923377c2b 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 5ee0a232c14b1d051f89939f09126f0664d056f6..cc4ced4bfa63230598d09324dd9cecdf25917646 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 a3a203eb6c7478a61e9b00e6cb453d8f211bda4f..28d3b1aac6194de68decb3aad592930d7d05c1d2 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 6d0cc9b254aacf4b66f52aa978d3e39177846932..f231fb042cb674fa3721a3af5e738e95e098f545 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 2e0c8f963873e4eb1135a5598f69923cadad9af9..b58e86cce5e522462e5d2c639c8cc7b8bee0eb27 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 a4c5684758293a710da3057a4b6d1a219bcc4541..efc57b6183b5975f7b8605af6ecacb8409e2fa88 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 00091d72a9fae928a52d6965cab2ccdbd78f4c97..ed869315385b0a55a80d94923101c8f805babcce 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 256b9a73626a1c86f0d1ddbecdaf65cd83998adf..5e7de78ee60a2f5aa14cc1f5e319aab15f01ab5e 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 2ead4dbe67bf2ca9f91899e0445d78ed0d950867..d46d52bdc2ca803b21d3faac80876001c715fc68 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 03f4311ee37648094fb88008f0bbfff5e15a250c..b732e6a34d538630c79489e85d1256b3a126eeb3 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 c106bd36a024823ff91e91579281a9285231941c..31f6983483faa6a1cf748b59de00f228305d5855 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 d582428d468340a9104a6d2f3d446e3db38d656b..34d7eb2a98234201feba0ed0c8ac99eb43f27da4 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 0eb3a6468cfa470ae0bf1b4f772a46855ac5633c..0e0ad91c1638620ed0195d7987d0fa01003e73c6 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 9ea4ec380dbcca9cc162fbb906b22ebd0f097475..13c02c6b2d165dd77354201d006bda6425925a7f 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 67c1fd0139e66e7d4a490b03b1ba294029d50bba..0db49291906bd53d4198f688cb412a1d48eceeab 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 03dd7d0a795315ea3aecd14749487693bbe9cfff..372e798b6738aa13ac1808713975884123dac150 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 47692e24e29916ec2333ca3db7f0bb23c9d4e40e..af0aea662d2da09f00b8ce7532b0d23648a6771c 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 2a4bfbb497570646f317a41905d153ff29edca5d..fe16dc545ec4bc400ffb2f52a45392edb2555020 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 a17c2fcf344a6a740af5e8b9f87f4cb6dea3765d..d0a1dcf567acd74de8f3d99a2045742ec76ea668 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 3917685de3c15a95a64243778479c7addc14ab1b..4f31df7dff83aa35c0fa9c26f3428671d4a1b5b5 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 8360b587599ccb94f2b024c53a2c5152fc3f5cc7..94c1cbf18655420babfe0f2e5252d44574767bc2 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 e317fb0d4fd3a542d7ec024c9030a6078fae9421..0cee2a2b63172d9a9266c3f665cb4bd8bd3a43b3 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 e1a7716376ac86b259906d61a332542ec08da136..70c1d992d17e288ca98283f4f7413b93496b1c8c 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 a41a5ede9f8b081ebb7299cef01116cb42eff42f..258e09a4a6956547a87e73fee12edb2644aaea3c 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
------------------------------------------------------------