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 ## Attachments - [wp2.c](/uploads/b42a155d1a7118131a8c4260a6a121b4/wp2.c)