Pb with annot.c in
ID0000440:
**This issue was created automatically from Mantis Issue 440. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000440 | Frama-C | Plug-in > jessie | public | 2010-04-04 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | gava | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | Frama-C Carbon-20101201-beta1 |
### Description :
If you use
frama-c -jessie annot.c
where annot.c (from /test/cil.) ==
int fact(int n) {
int r = 1 ;
while ( n > 0 ) {
//@ assert n > 0 ;
before:
r *= n-- ;
//@ assert r == \at(r*n,before) ;
}
return r ;
}
Computation of VCs...
File "why/annot.why", line 410, characters 74-82:
Unbound label 'before'
(which is true when looking the file)
### Additional Information :
The bug does not show up if the first assert is removed. So it seems the first assert "enclosed" the statement "before: r *= n-- ;"
Which means that the problem might come from the Frama-C parser itself, which might have built a wrong AST.
Virgile, any thoughts ?
issue