From 5214045916e92d61acd81e3817f0afe01a4d5ac9 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 23 Jun 2021 15:16:55 +0200
Subject: [PATCH] [wp] Fix trivial terminates proof display + count
---
src/plugins/wp/register.ml | 11 +++++++++--
.../oracle/terminates_call_options.1.res.oracle | 1 +
.../wp_acsl/oracle/terminates_formulae.res.oracle | 1 +
.../oracle/terminates_variant_option.0.res.oracle | 4 ++++
.../oracle/terminates_variant_option.1.res.oracle | 4 ++++
.../terminates_call_options.1.res.oracle | 3 ++-
.../oracle_qualif/terminates_formulae.res.oracle | 3 ++-
.../terminates_variant_option.0.res.oracle | 6 +++++-
.../terminates_variant_option.1.res.oracle | 6 +++++-
src/plugins/wp/wpAnnot.ml | 5 +++++
src/plugins/wp/wpAnnot.mli | 1 +
11 files changed, 39 insertions(+), 6 deletions(-)
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index 9bff55614bf..de651b862f8 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -182,6 +182,7 @@ let clear_scheduled () =
exercised := 0 ;
session := GOALS.empty ;
provers := PM.empty ;
+ WpAnnot.trivial_terminates := 0 ;
WpAnnot.unreachable_proved := 0 ;
WpAnnot.unreachable_failed := 0 ;
end
@@ -462,13 +463,19 @@ let do_report_scheduled () =
Wp_parameters.result "%d goal%s generated" !exercised plural
else
let total =
- !scheduled + !WpAnnot.unreachable_failed + !WpAnnot.unreachable_proved in
+ !scheduled +
+ !WpAnnot.unreachable_failed +
+ !WpAnnot.unreachable_proved +
+ !WpAnnot.trivial_terminates in
if total > 0 then
begin
+ let passed =
+ !WpAnnot.unreachable_proved + !WpAnnot.trivial_terminates
+ in
let passed = GOALS.fold
(fun g n ->
if Wpo.is_passed g then succ n else n
- ) !session !WpAnnot.unreachable_proved in
+ ) !session passed in
let mode = Cache.get_mode () in
if mode <> Cache.NoCache then do_report_cache_usage mode ;
Wp_parameters.result "%t"
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/terminates_call_options.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/terminates_call_options.1.res.oracle
index d367e2cc027..48a05c29bcb 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/terminates_call_options.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/terminates_call_options.1.res.oracle
@@ -4,6 +4,7 @@
[wp] Warning: Missing RTE guards
[wp] tests/wp_acsl/terminates_call_options.c:20: Warning:
Missing terminates clause for definition, populates 'terminates \true'
+[wp] [CFG] Goal definition_terminates : Valid (Trivial)
[wp] tests/wp_acsl/terminates_call_options.c:32: Warning:
Missing terminates clause for no_spec_generates_goal, populates 'terminates \true'
[wp] tests/wp_acsl/terminates_call_options.c:17: Warning:
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/terminates_formulae.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/terminates_formulae.res.oracle
index 81be3fb1362..ecb311b8fc1 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/terminates_formulae.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/terminates_formulae.res.oracle
@@ -2,6 +2,7 @@
[kernel] Parsing tests/wp_acsl/terminates_formulae.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
+[wp] [CFG] Goal variant_terminates : Valid (Trivial)
------------------------------------------------------------
Function base_call
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/terminates_variant_option.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/terminates_variant_option.0.res.oracle
index 758094faa1e..1d76571f54f 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/terminates_variant_option.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/terminates_variant_option.0.res.oracle
@@ -1,7 +1,11 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/terminates_variant_option.i (no preprocessing)
[wp] Running WP plugin...
+[wp] [CFG] Goal f1_terminates : Valid (Trivial)
[wp] Warning: Missing RTE guards
+[wp] [CFG] Goal fails_decreases_terminates : Valid (Trivial)
+[wp] [CFG] Goal fails_positive_terminates : Valid (Trivial)
+[wp] [CFG] Goal trivial_variant_terminates : Valid (Trivial)
------------------------------------------------------------
Function f1
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/terminates_variant_option.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/terminates_variant_option.1.res.oracle
index 2324adf7478..09103afc39d 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/terminates_variant_option.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/terminates_variant_option.1.res.oracle
@@ -1,9 +1,13 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/terminates_variant_option.i (no preprocessing)
[wp] Running WP plugin...
+[wp] [CFG] Goal f1_terminates : Valid (Trivial)
[wp] Warning: Missing RTE guards
+[wp] [CFG] Goal fails_decreases_terminates : Valid (Trivial)
+[wp] [CFG] Goal fails_positive_terminates : Valid (Trivial)
[wp] tests/wp_acsl/terminates_variant_option.i:52: Warning:
Loop variant is always trivially verified (terminates \false)
+[wp] [CFG] Goal trivial_variant_terminates : Valid (Trivial)
[wp] tests/wp_acsl/terminates_variant_option.i:59: Warning:
Loop variant is always trivially verified (terminates \false)
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_call_options.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_call_options.1.res.oracle
index e6da7db09de..5d8ea75da40 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_call_options.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_call_options.1.res.oracle
@@ -4,6 +4,7 @@
[wp] Warning: Missing RTE guards
[wp] tests/wp_acsl/terminates_call_options.c:20: Warning:
Missing terminates clause for definition, populates 'terminates \true'
+[wp] [CFG] Goal definition_terminates : Valid (Trivial)
[wp] tests/wp_acsl/terminates_call_options.c:32: Warning:
Missing terminates clause for no_spec_generates_goal, populates 'terminates \true'
[wp] tests/wp_acsl/terminates_call_options.c:17: Warning:
@@ -20,7 +21,7 @@
[wp] [Qed] Goal typed_call_definition_terminates : Valid
[wp] [Alt-Ergo] Goal typed_no_spec_generates_goal_terminates : Unsuccess
[wp] [Qed] Goal typed_libc_call_terminates : Valid
-[wp] Proved goals: 4 / 5
+[wp] Proved goals: 5 / 6
Qed: 4
Alt-Ergo: 0 (unsuccess: 1)
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_formulae.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_formulae.res.oracle
index 095b267c6ec..1793ed9f2e9 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_formulae.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_formulae.res.oracle
@@ -2,6 +2,7 @@
[kernel] Parsing tests/wp_acsl/terminates_formulae.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
+[wp] [CFG] Goal variant_terminates : Valid (Trivial)
[wp] 10 goals scheduled
[wp] [Alt-Ergo] Goal typed_base_call_terminates : Unsuccess
[wp] [Qed] Goal typed_call_same_terminates : Valid
@@ -13,7 +14,7 @@
[wp] [Qed] Goal typed_variant_loop_variant_positive : Valid
[wp] [Alt-Ergo] Goal typed_no_variant_terminates : Unsuccess
[wp] [Qed] Goal typed_no_variant_loop_assigns : Valid
-[wp] Proved goals: 6 / 10
+[wp] Proved goals: 7 / 11
Qed: 5
Alt-Ergo: 1 (unsuccess: 4)
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_variant_option.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_variant_option.0.res.oracle
index 927ca972024..35fe4fded76 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_variant_option.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_variant_option.0.res.oracle
@@ -1,7 +1,11 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/terminates_variant_option.i (no preprocessing)
[wp] Running WP plugin...
+[wp] [CFG] Goal f1_terminates : Valid (Trivial)
[wp] Warning: Missing RTE guards
+[wp] [CFG] Goal fails_decreases_terminates : Valid (Trivial)
+[wp] [CFG] Goal fails_positive_terminates : Valid (Trivial)
+[wp] [CFG] Goal trivial_variant_terminates : Valid (Trivial)
[wp] 20 goals scheduled
[wp] [Alt-Ergo] Goal typed_fails_positive_loop_invariant_preserved : Valid
[wp] [Qed] Goal typed_fails_positive_loop_invariant_established : Valid
@@ -23,7 +27,7 @@
[wp] [Qed] Goal typed_trivial_variant_default_loop_assigns : Valid
[wp] [Alt-Ergo] Goal typed_trivial_variant_default_loop_variant_decrease : Unsuccess
[wp] [Alt-Ergo] Goal typed_trivial_variant_default_loop_variant_positive : Unsuccess
-[wp] Proved goals: 13 / 20
+[wp] Proved goals: 17 / 24
Qed: 10
Alt-Ergo: 3 (unsuccess: 7)
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_variant_option.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_variant_option.1.res.oracle
index f7c77c67df3..fa298976b2b 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_variant_option.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_variant_option.1.res.oracle
@@ -1,9 +1,13 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/terminates_variant_option.i (no preprocessing)
[wp] Running WP plugin...
+[wp] [CFG] Goal f1_terminates : Valid (Trivial)
[wp] Warning: Missing RTE guards
+[wp] [CFG] Goal fails_decreases_terminates : Valid (Trivial)
+[wp] [CFG] Goal fails_positive_terminates : Valid (Trivial)
[wp] tests/wp_acsl/terminates_variant_option.i:52: Warning:
Loop variant is always trivially verified (terminates \false)
+[wp] [CFG] Goal trivial_variant_terminates : Valid (Trivial)
[wp] tests/wp_acsl/terminates_variant_option.i:59: Warning:
Loop variant is always trivially verified (terminates \false)
[wp] 20 goals scheduled
@@ -27,7 +31,7 @@
[wp] [Qed] Goal typed_trivial_variant_default_loop_assigns : Valid
[wp] [Qed] Goal typed_trivial_variant_default_loop_variant_decrease : Valid
[wp] [Qed] Goal typed_trivial_variant_default_loop_variant_positive : Valid
-[wp] Proved goals: 20 / 20
+[wp] Proved goals: 24 / 24
Qed: 16
Alt-Ergo: 4
------------------------------------------------------------
diff --git a/src/plugins/wp/wpAnnot.ml b/src/plugins/wp/wpAnnot.ml
index 71fe8e549cb..7f6b34561c7 100644
--- a/src/plugins/wp/wpAnnot.ml
+++ b/src/plugins/wp/wpAnnot.ml
@@ -79,6 +79,9 @@ let set_unreachable pid =
(* -------------------------------------------------------------------------- *)
(* --- Status of Terminates Annotations --- *)
(* -------------------------------------------------------------------------- *)
+
+let trivial_terminates = ref 0
+
let wp_trivially_terminates =
Emitter.create
"Trivial Termination"
@@ -87,6 +90,8 @@ let wp_trivially_terminates =
~tuning:[] (* TBC *)
let set_trivially_terminates p =
+ incr trivial_terminates ;
+ Wp_parameters.result "[CFG] Goal %a : Valid (Trivial)" WpPropId.pp_propid p ;
let pid = WpPropId.property_of_id p in
Property_status.emit wp_trivially_terminates ~hyps:[] pid Property_status.True
diff --git a/src/plugins/wp/wpAnnot.mli b/src/plugins/wp/wpAnnot.mli
index e08e70cdcbc..171a83e4299 100644
--- a/src/plugins/wp/wpAnnot.mli
+++ b/src/plugins/wp/wpAnnot.mli
@@ -34,6 +34,7 @@ open Cil_types
val unreachable_proved : int ref
val unreachable_failed : int ref
+val trivial_terminates : int ref
val set_unreachable : WpPropId.prop_id -> unit
val set_trivially_terminates : WpPropId.prop_id -> unit
--
GitLab