ID0001353: **This issue was created automatically from Mantis Issue 1353. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0001353 | Frama-C | Plug-in > wp | public | 2013-01-30 | 2014-03-13 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | Anne | **Assigned To** | correnson | **Resolution** | fixed | | **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried | | **Platform** | - | **OS** | - | **OS Version** | - | | **Product Version** | Frama-C Oxygen-20120901 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 | ### Description : As said in the title, the ACSL label LoopEntry seems to be not handled by WP but it is accepted by the kernel. Using the -wp-warnings option I got warnings like : - Warning: Generalization of un-labeled values Reason: Some labels may escape the control flow but it took me some time to understand the problem. In the example below, changing LoopEntry by L in the loop invariant makes it work. BTW, in the example below, it doesn't work either when removing the first (c++;) statement ! ### Additional Information : int G; //@ requires G == 0; ensures G == 0; void f (int c) { c++; L: //@ loop invariant G == \at (G, LoopEntry); while (c) c++; }