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.
|ID0001911||Frama-C||Plug-in > wp||public||2014-08-19||2016-03-07|
|Priority||normal||Severity||minor||Reproducibility||have not tried|
|Product Version||-||Target Version||-||Fixed in Version||-|
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
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information