double struct dereferencing causes unbound variable error
ID0000811: This issue was created automatically from Mantis Issue 811. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000811 | Frama-C | Plug-in > jessie | public | 2011-05-02 | 2011-05-06 |
| Reporter | Jochen | Assigned To | cmarche | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Carbon-20110201 | Target Version | - | Fixed in Version | - |
Description :
Jessie reports <<File "why/ftest.why", line 371, characters 25-51: Unbound variable _elem_e_1_alloc_table>> for the attached program. Adding a "requires \valid(e)" makes the error message disappear.
The code in the procedure body does not require the validity of e. It does not assign anything outside of e->next->next, so the "assigns" clause is overestimating, but correct. Therefor, Jessie should not report an error.
Attachments
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information