WP detect a non-natural loop on a do-while(0) loop
ID0001911: This issue was created automatically from Mantis Issue 1911. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001911 | Frama-C | Plug-in > wp | public | 2014-08-19 | 2016-03-07 |
| Reporter | Anne | Assigned To | correnson | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | have not tried |
| Platform | - | OS | - | OS Version | - |
| Product Version | - | Target Version | - | Fixed in Version | - |
Description :
In 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 ?
Additional Information :
It is ok with -wp-invariants option.
Steps To Reproduce :
$ frama-c -wp-fct main wp2.c