From 26cdb440d93dbe4a766e1739d2d1721204fd5ceb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 17 Feb 2021 14:12:04 +0100
Subject: [PATCH] [wp] removed arbitrary loops
---
src/plugins/wp/tests/wp_bts/issue_141.i | 29 -------------------
.../tests/wp_bts/oracle/issue_141.res.oracle | 10 -------
2 files changed, 39 deletions(-)
delete mode 100644 src/plugins/wp/tests/wp_bts/issue_141.i
delete mode 100644 src/plugins/wp/tests/wp_bts/oracle/issue_141.res.oracle
diff --git a/src/plugins/wp/tests/wp_bts/issue_141.i b/src/plugins/wp/tests/wp_bts/issue_141.i
deleted file mode 100644
index 10dfcd1a1e2..00000000000
--- a/src/plugins/wp/tests/wp_bts/issue_141.i
+++ /dev/null
@@ -1,29 +0,0 @@
-/* run.config
- OPT: -wp-rte -wp -wp-steps 50
-*/
-/* run.config_qualif
- DONTRUN:
-*/
-
-typedef struct list { struct list *next; };
-struct list *cur;
-
-volatile int nondet;
-
-void f(int i) {}
-
-int main() {
- int bla = -1;
- reset:
- if (nondet) f(bla);
- while (nondet) {
- if (nondet) goto reset;
- if (nondet) goto exit;
- }
- goto reset;
- exit:
- while (nondet) {
- cur = cur->next;
- }
- return 0;
-}
diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_141.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_141.res.oracle
deleted file mode 100644
index 9dd3dd748e7..00000000000
--- a/src/plugins/wp/tests/wp_bts/oracle/issue_141.res.oracle
+++ /dev/null
@@ -1,10 +0,0 @@
-# frama-c -wp -wp-rte -wp-steps 50 [...]
-[kernel] Parsing tests/wp_bts/issue_141.i (no preprocessing)
-[wp] Running WP plugin...
-[rte] annotating function f
-[rte] annotating function main
-[wp] tests/wp_bts/issue_141.i:18: Warning:
- calculus failed on strategy
- for 'main', behavior 'default!', all properties, both assigns or not because
- unsupported strange loop(s). (abort)
-[wp] No proof obligations
--
GitLab