GitLab

ID0001281: This issue was created automatically from Mantis Issue 1281. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0001281	Frama-C	Plug-in > wp	public	2012-10-15	2014-02-05

Reporter	sjw	Assigned To	correnson	Resolution	open
Priority	normal	Severity	minor	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Oxygen-20120901	Target Version	-	Fixed in Version	-

Description :

The pattern do { ... } while (0) is used in a number of standard headers to allow pre-processor macros to introduce a scope and still look like a statement (you can put a semi-colon after them). This translates to something like while(1) { ...; break; } as in the following

/*@ requires \valid(x); @ ensures \result == 0; */ int foo(int *x) {

/* loop invariant 0 == 0; */
while( 1 ) {
    *x = 0;
    break;

}

return *x;

}

which fails with $ frama-c -wp do_while_test.c [kernel] preprocessing with "gcc -C -E -I. do_while_test.c" [wp] Running WP plugin... [wp] Collecting axiomatic usage [wp] warning: Missing RTE guards do_while_test.c:6:[wp] warning: calculus failed on strategy for 'foo', behavior 'default!', all properties, both assigns or not because unsupported non-natural loop without invariant property. (abort) [wp] 0 goal scheduled

It looks like the unconditional break (i.e., the results of optimising if (!0) break; from the translation of the 'do') causes the cil2cfg pass to throw out some loop edges, causing the above error.