Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001281Frama-CPlug-in > wppublic2012-10-15 08:372014-02-05 17:45
Reportersjw 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusacknowledgedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Oxygen-20120901 
Target VersionFixed in Version 
Summary0001281: 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.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0004510)
correnson (manager)
2014-02-05 17:00

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
2014-02-05 17:45 correnson Relationship added has duplicate 0001491


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker