2021-01-17 22:48 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001281Frama-CPlug-in > wppublic2014-02-05 17:45
Assigned Tocorrenson 
Product VersionFrama-C Oxygen-20120901 
Target VersionFixed in Version 
Summary0001281: do { ... } while (0) pattern causes wp to fail
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;

    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.
TagsNo tags attached.
Attached Files




correnson (manager)

To be fixed with the restructuration of WP calculus.

-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