labels defined before loops and used after loops are not correctly translated in jessie
ID0001047:
**This issue was created automatically from Mantis Issue 1047. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001047 | Frama-C | Plug-in > jessie | public | 2011-12-12 | 2011-12-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | chernikova | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | - |
### Description :
An example with a label in a ghost (or not) statement:
void main(){
int p = 1;
int i;
//@ ghost L:
for (i=0; i<10; i++)
p = 2;
//@ assert \at(p,L)==p-1;
}
frama-c -jessie labels-bug.c results as:
...
File "labels-bug.jc", line 52, characters 38-46: typing error: label `L' not found
...
labels-bug.jc contains label L:
....
(C_1 : (p = 1));
(L : ());
(C_2 : (i = 0));
loop
while (true)
{
...
};
(while_0_break : ());
{
(assert for default: (C_7 : (\at(p,L) == (p - 1))));
()
};
## Attachments
- [labels-bug.c](/uploads/c63651c10d36026a0949f7dda5a96ae8/labels-bug.c)
issue