Skip to content
Snippets Groups Projects
Commit 26cdb440 authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[wp] removed arbitrary loops

parent 8d909d29
No related branches found
No related tags found
No related merge requests found
/* 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;
}
# 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
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment