Skip to content

GitLab

  • Menu
Projects Groups Snippets
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 208
    • Issues 208
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #1816

Closed
Open
Created Oct 15, 2012 by mantis-gitlab-migration@mantis-gitlab-migration

do { ... } while (0) pattern causes wp to fail

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.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking