Skip to content
Snippets Groups Projects
Commit c635c818 authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[wp] emit a warning when no generated goal

parent 78e6d5e5
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 39 additions and 53 deletions
src/plugins/wp/Changelog
+ 1
− 0
View file @ c635c818
......@@ -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)
......
src/plugins/wp/register.ml
+ 20
− 17
View file @ c635c818
......@@ -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
......
src/plugins/wp/tests/wp_plugin/oracle_qualif/nowp.res.oracle
+ 1
− 2
View file @ c635c818
......@@ -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
------------------------------------------------------------
src/plugins/wp/tests/wp_plugin/oracle_qualif/removed.res.oracle
+ 1
− 2
View file @ c635c818
......@@ -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
src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.2.res.oracle
+ 1
− 2
View file @ c635c818
......@@ -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
------------------------------------------------------------
src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.log
+ 1
− 2
View file @ c635c818
......@@ -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
src/plugins/wp/tests/wp_region/oracle_qualif/array1.res.oracle
+ 1
− 2
View file @ c635c818
......@@ -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
------------------------------------------------------------
src/plugins/wp/tests/wp_region/oracle_qualif/array2.res.oracle
+ 1
− 2
View file @ c635c818
......@@ -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
------------------------------------------------------------
src/plugins/wp/tests/wp_region/oracle_qualif/array3.res.oracle
+ 1
− 2
View file @ c635c818
......@@ -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
------------------------------------------------------------
src/plugins/wp/tests/wp_region/oracle_qualif/array4.res.oracle
+ 1
− 2
View file @ c635c818
......@@ -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
------------------------------------------------------------
src/plugins/wp/tests/wp_region/oracle_qualif/array5.res.oracle
+ 1
− 2
View file @ c635c818
......@@ -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
------------------------------------------------------------
src/plugins/wp/tests/wp_region/oracle_qualif/array6.res.oracle
+ 1
− 2
View file @ c635c818
......@@ -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
------------------------------------------------------------
src/plugins/wp/tests/wp_region/oracle_qualif/array7.res.oracle
+ 1
− 2
View file @ c635c818
......@@ -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
------------------------------------------------------------
src/plugins/wp/tests/wp_region/oracle_qualif/array8.res.oracle
+ 1
− 2
View file @ c635c818
......@@ -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
------------------------------------------------------------
src/plugins/wp/tests/wp_region/oracle_qualif/fb_ADD.res.oracle
+ 1
− 2
View file @ c635c818
......@@ -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
------------------------------------------------------------
src/plugins/wp/tests/wp_region/oracle_qualif/fb_SORT.res.oracle
+ 1
− 2
View file @ c635c818
......@@ -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
------------------------------------------------------------
src/plugins/wp/tests/wp_region/oracle_qualif/garbled.res.oracle
+ 1
− 2
View file @ c635c818
......@@ -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
------------------------------------------------------------
src/plugins/wp/tests/wp_region/oracle_qualif/index.res.oracle
+ 1
− 2
View file @ c635c818
......@@ -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
------------------------------------------------------------
src/plugins/wp/tests/wp_region/oracle_qualif/matrix.res.oracle
+ 1
− 2
View file @ c635c818
......@@ -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
------------------------------------------------------------
src/plugins/wp/tests/wp_region/oracle_qualif/structarray1.res.oracle
+ 1
− 2
View file @ c635c818
......@@ -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
------------------------------------------------------------
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment