From 244d85f23e2f472262b19852d5dff8a645d94784 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 18 Feb 2021 09:53:25 +0100
Subject: [PATCH] [wp] removed stmt-contract
---
src/plugins/wp/tests/wp_bts/issue_453.i | 35 --------------
.../tests/wp_bts/oracle/issue_453.res.oracle | 46 -------------------
.../wp_bts/oracle_qualif/issue_453.res.oracle | 18 --------
3 files changed, 99 deletions(-)
delete mode 100644 src/plugins/wp/tests/wp_bts/issue_453.i
delete mode 100644 src/plugins/wp/tests/wp_bts/oracle/issue_453.res.oracle
delete mode 100644 src/plugins/wp/tests/wp_bts/oracle_qualif/issue_453.res.oracle
diff --git a/src/plugins/wp/tests/wp_bts/issue_453.i b/src/plugins/wp/tests/wp_bts/issue_453.i
deleted file mode 100644
index af0f2ff6923..00000000000
--- a/src/plugins/wp/tests/wp_bts/issue_453.i
+++ /dev/null
@@ -1,35 +0,0 @@
-typedef unsigned T;
-T incr_value;
-
-//@ axiomatic A { predicate Incr(T x, T r) = r == x + incr_value; }
-
-/*@ assigns \nothing;
- @ ensures Incr(x, \result);
- @ */
-T incr(T x);
-
-// Was KO before the fix of #453
-void f1(T i) {
- /*@ loop assigns i;
- @*/
- while (i<10) {
- /*@ assigns i ;
- ensures Sincr: Incr(\old(i), i);
- */
- i = incr(i);
- }
-}
-
-// Was OK before the fix of #453
-void f2(T i) {
- /*@ loop assigns i;
- @*/
- while (i<10) {
- //@ ghost A: ;
- /*@ assigns i ;
- ensures Sincr: Incr(\old(i), i);
- */
- i = incr(i);
- //@ ghost B: ;
- }
-}
diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_453.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_453.res.oracle
deleted file mode 100644
index 9c1dde973cc..00000000000
--- a/src/plugins/wp/tests/wp_bts/oracle/issue_453.res.oracle
+++ /dev/null
@@ -1,46 +0,0 @@
-# frama-c -wp [...]
-[kernel] Parsing tests/wp_bts/issue_453.i (no preprocessing)
-[wp] Running WP plugin...
-[wp] Warning: Missing RTE guards
-------------------------------------------------------------
- Function f1
-------------------------------------------------------------
-
-Goal Loop assigns (file tests/wp_bts/issue_453.i, line 13):
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function f1 with behavior default_for_stmt_7
-------------------------------------------------------------
-
-Goal Post-condition 'Sincr' at call 'incr' (file tests/wp_bts/issue_453.i, line 19):
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns (file tests/wp_bts/issue_453.i, line 16) at call 'incr' (file tests/wp_bts/issue_453.i, line 19):
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function f2
-------------------------------------------------------------
-
-Goal Loop assigns (file tests/wp_bts/issue_453.i, line 25):
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function f2 with behavior default_for_stmt_17
-------------------------------------------------------------
-
-Goal Post-condition 'Sincr' at call 'incr' (file tests/wp_bts/issue_453.i, line 32):
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns (file tests/wp_bts/issue_453.i, line 29) at call 'incr' (file tests/wp_bts/issue_453.i, line 32):
-Prove: true.
-
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_453.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_453.res.oracle
deleted file mode 100644
index c4d33cc9b69..00000000000
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_453.res.oracle
+++ /dev/null
@@ -1,18 +0,0 @@
-# frama-c -wp [...]
-[kernel] Parsing tests/wp_bts/issue_453.i (no preprocessing)
-[wp] Running WP plugin...
-[wp] Warning: Missing RTE guards
-[wp] 6 goals scheduled
-[wp] [Qed] Goal typed_f1_loop_assigns : Valid
-[wp] [Qed] Goal typed_f1_ensures_Sincr : Valid
-[wp] [Qed] Goal typed_f1_assigns : Valid
-[wp] [Qed] Goal typed_f2_loop_assigns : Valid
-[wp] [Qed] Goal typed_f2_ensures_Sincr : Valid
-[wp] [Qed] Goal typed_f2_assigns : Valid
-[wp] Proved goals: 6 / 6
- Qed: 6
-------------------------------------------------------------
- Functions WP Alt-Ergo Total Success
- f1 3 - 3 100%
- f2 3 - 3 100%
-------------------------------------------------------------
--
GitLab