#defined variable unrecognized in assigns, except in parentheses
ID0001019: This issue was created automatically from Mantis Issue 1019. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001019 | Frama-C | Kernel > ACSL implementation | public | 2011-11-16 | 2012-09-19 |
| Reporter | Jochen | Assigned To | virgile | Resolution | no change required |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Nitrogen-20111001 | Target Version | - | Fixed in Version | Frama-C Oxygen-20120901 |
Description :
Frama-C reports a kernel error "unbound logic variable n in annotation" when run on the attached program. The error occurs when Jessie (why 2.30) is used, and also when Wp is used.
Note that "n" is accepted in the requires clause. If the assigns clause is changed to "assigns a[0..(n)];", the error disappears.