From d3b8510aa3cfd54ce256a94d55d32c07d6a821a6 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 3 Jun 2021 15:33:57 +0200
Subject: [PATCH] [wp] Add terminates variant test
---
.../terminates_variant_option.0.res.oracle | 58 +++++++++++++++++++
.../terminates_variant_option.1.res.oracle | 53 +++++++++++++++++
.../terminates_variant_option.0.res.oracle | 15 +++--
.../terminates_variant_option.1.res.oracle | 15 +++--
.../tests/wp_acsl/terminates_variant_option.i | 15 +++++
5 files changed, 148 insertions(+), 8 deletions(-)
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 ed3edfb084b..4c0590685f6 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
@@ -2,6 +2,64 @@
[kernel] Parsing tests/wp_acsl/terminates_variant_option.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function f1
+------------------------------------------------------------
+
+Goal Termination-condition (file tests/wp_acsl/terminates_variant_option.i, line 34) in 'f1':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant (file tests/wp_acsl/terminates_variant_option.i, line 37):
+Assume {
+ Type: is_sint32(c1_0) /\ is_sint32(cpt_0) /\ is_sint32(cpt_0 - 1).
+ (* Residual *)
+ When: c1_0 != 0.
+ (* Goal *)
+ When: 0 <= c1_0.
+ (* Invariant *)
+ Have: (cpt_0 <= c1_0) /\ (0 <= cpt_0).
+ (* Else *)
+ Have: 2 <= cpt_0.
+}
+Prove: (0 < cpt_0) /\ (cpt_0 <= (1 + c1_0)).
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant (file tests/wp_acsl/terminates_variant_option.i, line 37):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_acsl/terminates_variant_option.i, line 38):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Decreasing of Loop variant at loop (file tests/wp_acsl/terminates_variant_option.i, line 41):
+Assume {
+ Type: is_sint32(cpt_0).
+ (* Invariant *)
+ Have: (cpt_0 <= 0) /\ (0 <= cpt_0).
+}
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Positivity of Loop variant at loop (file tests/wp_acsl/terminates_variant_option.i, line 41):
+Assume {
+ Type: is_sint32(c1_0) /\ is_sint32(cpt_0) /\ is_sint32(cpt_0 - 1).
+ (* Residual *)
+ When: c1_0 != 0.
+ (* Invariant *)
+ Have: ((0 <= c1_0) -> ((cpt_0 <= c1_0) /\ (0 <= cpt_0))).
+ (* Else *)
+ Have: 2 <= cpt_0.
+}
+Prove: 0 <= cpt_0.
+
+------------------------------------------------------------
------------------------------------------------------------
Function fails_decreases
------------------------------------------------------------
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 c7b38328fe5..9b9f856e6c3 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
@@ -2,6 +2,59 @@
[kernel] Parsing tests/wp_acsl/terminates_variant_option.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function f1
+------------------------------------------------------------
+
+Goal Termination-condition (file tests/wp_acsl/terminates_variant_option.i, line 34) in 'f1':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant (file tests/wp_acsl/terminates_variant_option.i, line 37):
+Assume {
+ Type: is_sint32(c1_0) /\ is_sint32(cpt_0) /\ is_sint32(cpt_0 - 1).
+ (* Residual *)
+ When: c1_0 != 0.
+ (* Goal *)
+ When: 0 <= c1_0.
+ (* Invariant *)
+ Have: (cpt_0 <= c1_0) /\ (0 <= cpt_0).
+ (* Else *)
+ Have: 2 <= cpt_0.
+}
+Prove: (0 < cpt_0) /\ (cpt_0 <= (1 + c1_0)).
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant (file tests/wp_acsl/terminates_variant_option.i, line 37):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_acsl/terminates_variant_option.i, line 38):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Decreasing of Loop variant at loop (file tests/wp_acsl/terminates_variant_option.i, line 41):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Positivity of Loop variant at loop (file tests/wp_acsl/terminates_variant_option.i, line 41):
+Assume {
+ Type: is_sint32(c1_0) /\ is_sint32(cpt_0) /\ is_sint32(cpt_0 - 1).
+ (* Goal *)
+ When: c1_0 != 0.
+ (* Invariant *)
+ Have: ((0 <= c1_0) -> ((cpt_0 <= c1_0) /\ (0 <= cpt_0))).
+ (* Else *)
+ Have: 2 <= cpt_0.
+}
+Prove: 0 <= cpt_0.
+
+------------------------------------------------------------
------------------------------------------------------------
Function fails_decreases
------------------------------------------------------------
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 3d7432f4f67..ed6365ffa37 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
@@ -2,7 +2,7 @@
[kernel] Parsing tests/wp_acsl/terminates_variant_option.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp] 11 goals scheduled
+[wp] 17 goals scheduled
[wp] [Qed] Goal typed_fails_positive_terminates : Valid
[wp] [Alt-Ergo] Goal typed_fails_positive_loop_invariant_preserved : Valid
[wp] [Qed] Goal typed_fails_positive_loop_invariant_established : Valid
@@ -14,11 +14,18 @@
[wp] [Qed] Goal typed_fails_decreases_loop_assigns : Valid
[wp] [Alt-Ergo] Goal typed_fails_decreases_loop_variant_decrease : Unsuccess
[wp] [Qed] Goal typed_fails_decreases_loop_variant_positive : Valid
-[wp] Proved goals: 9 / 11
- Qed: 8
- Alt-Ergo: 1 (unsuccess: 2)
+[wp] [Qed] Goal typed_f1_terminates : Valid
+[wp] [Alt-Ergo] Goal typed_f1_loop_invariant_preserved : Valid
+[wp] [Qed] Goal typed_f1_loop_invariant_established : Valid
+[wp] [Qed] Goal typed_f1_loop_assigns : Valid
+[wp] [Alt-Ergo] Goal typed_f1_loop_variant_decrease : Unsuccess
+[wp] [Alt-Ergo] Goal typed_f1_loop_variant_positive : Valid
+[wp] Proved goals: 14 / 17
+ Qed: 11
+ Alt-Ergo: 3 (unsuccess: 3)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
fails_positive 5 1 7 85.7%
fails_decreases 3 - 4 75.0%
+ f1 3 2 6 83.3%
------------------------------------------------------------
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 4724528d6f0..c7928a6b12e 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
@@ -2,7 +2,7 @@
[kernel] Parsing tests/wp_acsl/terminates_variant_option.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp] 11 goals scheduled
+[wp] 17 goals scheduled
[wp] [Qed] Goal typed_fails_positive_terminates : Valid
[wp] [Alt-Ergo] Goal typed_fails_positive_loop_invariant_preserved : Valid
[wp] [Qed] Goal typed_fails_positive_loop_invariant_established : Valid
@@ -14,11 +14,18 @@
[wp] [Qed] Goal typed_fails_decreases_loop_assigns : Valid
[wp] [Alt-Ergo] Goal typed_fails_decreases_loop_variant_decrease : Valid
[wp] [Qed] Goal typed_fails_decreases_loop_variant_positive : Valid
-[wp] Proved goals: 11 / 11
- Qed: 9
- Alt-Ergo: 2
+[wp] [Qed] Goal typed_f1_terminates : Valid
+[wp] [Alt-Ergo] Goal typed_f1_loop_invariant_preserved : Valid
+[wp] [Qed] Goal typed_f1_loop_invariant_established : Valid
+[wp] [Qed] Goal typed_f1_loop_assigns : Valid
+[wp] [Qed] Goal typed_f1_loop_variant_decrease : Valid
+[wp] [Alt-Ergo] Goal typed_f1_loop_variant_positive : Valid
+[wp] Proved goals: 17 / 17
+ Qed: 13
+ Alt-Ergo: 4
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
fails_positive 6 1 7 100%
fails_decreases 3 1 4 100%
+ f1 4 2 6 100%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/terminates_variant_option.i b/src/plugins/wp/tests/wp_acsl/terminates_variant_option.i
index 872b0734b8f..e220801f80a 100644
--- a/src/plugins/wp/tests/wp_acsl/terminates_variant_option.i
+++ b/src/plugins/wp/tests/wp_acsl/terminates_variant_option.i
@@ -30,3 +30,18 @@ void fails_decreases(int keep_going){
if(! keep_going) i-- ;
}
}
+
+//@ terminates c1 != 0;
+void f1 (int c1, int c2) {
+ int cpt = c1 ;
+ /*@ loop invariant c1 >= 0 ==> 0 <= cpt <= c1 ;
+ @ loop assigns cpt ;
+ @ loop variant cpt ;
+ @*/
+ while (1) {
+ if (c1 || c2) {
+ cpt --;
+ if (cpt <= 0) break;
+ }
+ }
+}
--
GitLab