| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 0001281 | Frama-C | Plug-in > wp | public | 2012-10-15 08:37 | 2014-02-05 17:45 | ||||||||
| Reporter | sjw | ||||||||||||
| Assigned To | correnson | ||||||||||||
| Priority | normal | Severity | minor | Reproducibility | always | ||||||||
| Status | acknowledged | Resolution | open | ||||||||||
| Product Version | Frama-C Oxygen-20120901 | ||||||||||||
| Target Version | Fixed in Version | ||||||||||||
| Summary | 0001281: do { ... } while (0) pattern causes wp to fail | ||||||||||||
| 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. | ||||||||||||
| Tags | No tags attached. | ||||||||||||
| Attached Files |
| ||||||||||||
 Relationships |
|
 Relationships |
| Notes |
|
|
correnson (manager) 2014-02-05 17:00 |
To be fixed with the restructuration of WP calculus. |
| Notes |
| Issue History |
|||
| Date Modified | Username | Field | Change |
|---|---|---|---|
| 2012-10-15 08:37 | sjw | New Issue | |
| 2012-10-15 08:37 | sjw | Status | new => assigned |
| 2012-10-15 08:37 | sjw | Assigned To | => correnson |
| 2014-02-05 17:00 | correnson | Note Added: 0004510 | |
| 2014-02-05 17:01 | correnson | Status | assigned => acknowledged |
| Issue History |