Jessie incorrectly handles labels
ID0001058: This issue was created automatically from Mantis Issue 1058. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001058 | Frama-C | Plug-in > jessie | public | 2012-01-04 | 2012-01-04 |
| Reporter | virgile | Assigned To | cmarche | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | have not tried |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C GIT, precise the release id | Target Version | - | Fixed in Version | - |
Description :
When using \at(x,L) in annotation where L is a C label, Jessie does not put the label at its correct place, resulting in unprovable formulæ.
Steps To Reproduce :
Starting from the following file:
int f(void) {
int x = 0; L: x++; //@ assert \at(x,L) == x - 1;
}
frama-c -jessie -jessie-why-opt="-tc" bug.i file.i
produces a correct file.jessie/file.jc but an incorrect file.jessie/why/file.why (label L gets placed at the beginning of the function).