diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index 9bff55614bf71b2281a5e671c08bc725efe3aed9..de651b862f8562d244218dabee2dba8dd3cb4a57 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 d367e2cc0273a670ded48578681bfd4deca900ad..48a05c29bcbcdcd40bae6cb2b8a769b3b45a7c89 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 81be3fb1362e31a592be0d542d697f4a5ba3cfd7..ecb311b8fc15f05a1cd4e543fceee46363f55a42 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 758094faa1e6ce02e1f5ce5816879f14b4ed873f..1d76571f54f0b012c92a2247df2716515527d399 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 2324adf7478aa37f9d7b0550d660da73ec08cc2f..09103afc39da2717b28b4744b2012e293889b894 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 e6da7db09def2a410052da6763e8aa3f9a3056c6..5d8ea75da400d6214a3258eff154a4aa18a4e934 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 095b267c6ecfc224c36136eb75184278762404af..1793ed9f2e90518b16e33e36f8b15690c411925d 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 927ca97202401004bf5b0f9578b5c9efbec6f9e5..35fe4fded760808fbfbce130caa38d2910f01a03 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 f7c77c67df30f8aab6e71ff53c3dea05e61ec333..fa298976b2b10f33fb419070f3988e046c18338a 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 71fe8e549cb6134eba6418ba7857cab7a9b8fde5..7f6b34561c7a477d185f523f4a2062febb460a50 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 e08e70cdcbc4bd48725473e81072d82158c75aa9..171a83e4299dd5991544d77a0d13e102a0a1c3e3 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