struct dereferencing causes uncaught exception
ID0000813: This issue was created automatically from Mantis Issue 813. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000813 | Frama-C | Plug-in > jessie | public | 2011-05-09 | 2011-05-09 |
| 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 an uncaught exception "Unexpected internal region in logic" when run on the attached program.
If the definition of "IsList" is expanded, i.e. if line 16 is used as the contract rather than line 15, the error message changes to "Unbound variable _elem_next_Last_12", coming from why. This behavior resembles to that reported in issue #811.
If axiom a1 in line 8 is activated rather than commented out, the error disappears in both cases (contract line 15/16).