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 10dfcd1a1e22a9f81272ff07eb66289f539774a9..0000000000000000000000000000000000000000 --- 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 9dd3dd748e7ee050326d660ce198563a2c639db4..0000000000000000000000000000000000000000 --- 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