clause "n<9-1" normalized to "n-1<9"
ID0001810: This issue was created automatically from Mantis Issue 1810. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001810 | Frama-Clang | Plug-in > clang | public | 2014-06-16 | 2014-06-19 |
| Reporter | Jochen | Assigned To | virgile | Resolution | fixed |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | - | OS | xubuntu-cfe13.10 | OS Version | - |
| Product Version | - | Target Version | - | Fixed in Version | Frama-C GIT, precise the release id |
Description :
Running "frama-c-gui -wp -wp-rte 108.cpp -wp-out wp-out" on the attached program shows in the gui's normalized-code window the clause "requires 0 <= n-1 && n-1 < 9;" as translation of source line 5 ("requires 0 <= n < 9-1;").
The same error is found in alt-ergo's input file "_Z4push_assert_rte_index_bound_2.ergo". As a consequence, alt-ergo can't prove the index bound for line 9.
The error disappears if
- the file is renamed to "108.c",
- "9-1" is replaced by "9" in line 5. The error appears unchanged if "n" is made a procedure parameter of "push".