array access in "decreases"-clause causes "Unexpected internal region in logic"
ID0000846: This issue was created automatically from Mantis Issue 846. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000846 | Frama-C | Plug-in > jessie | public | 2011-05-30 | 2011-05-30 |
| 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: Failure("Unexpected internal region in logic") on the attached file. That message vanishes if either
- the array access "b[f]" in line 4 is replaced e.g. by "0",
- the "decreases" clause in line 8 is deleted, or
- the recursive call in line 11 is deleted.
(The code is nonsensical, but has been boiled down from a reasonable program.)