Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001911Frama-CPlug-in > wppublic2014-08-19 11:112016-03-07 20:09
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityhave not tried
PlatformOSOS Version
Product Version 
Target VersionFixed in Version 
Summary0001911: WP detect a non-natural loop on a do-while(0) loop
DescriptionIn the attached example, the do-while(0) "false" loop makes the WP fail with the message: wp2.c:8:[wp] warning: calculus failed on strategy for 'main', behavior 'default!', all properties, both assigns or not because unsupported non-natural loop without invariant property. (abort) Maybe it can be detected that this is not a loop in fact ?
Steps To Reproduce$ frama-c -wp-fct main wp2.c
Additional InformationIt is ok with -wp-invariants option.
TagsNo tags attached.
Attached Filesc file icon wp2.c [^] (183 bytes) 2014-08-19 11:11 [Show Content]

- Relationships

-  Notes
correnson (manager)
2014-09-23 10:14

Yes, we have planned to reimplement the CFG used by WP to handle such corner cases. But the roadmap is long before having such as feature. In the meanwhile, it may be implemented as a small plugin that replaces do-while(0) into a simple block, and replaces breaks by goto.
correnson (manager)
2014-09-23 10:14

Feature wish
yakobowski (manager)
2016-03-07 20:09

Although the syntactic transformation has been implemented in the kernel (option -simplify-trivial-loops), it does not work when there is a break in the loop. So this example is still not ok. The kernel should probably improved to transform the break into a Goto, as suggested by Loïc.

- Issue History
Date Modified Username Field Change
2014-08-19 11:11 Anne New Issue
2014-08-19 11:11 Anne Status new => assigned
2014-08-19 11:11 Anne Assigned To => correnson
2014-08-19 11:11 Anne File Added: wp2.c
2014-09-23 10:14 correnson Note Added: 0005480
2014-09-23 10:14 correnson Note Added: 0005481
2014-09-23 10:14 correnson Status assigned => acknowledged
2016-03-07 20:09 yakobowski Note Added: 0006168

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker