variable declared in "for" init-part unrecognized in loop body assigns clause; 100% verification degree reported nevertheless
ID0002363: This issue was created automatically from Mantis Issue 2363. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002363 | Frama-C | Plug-in > clang | public | 2018-02-12 | 2018-02-12 |
| Reporter | Jochen | Assigned To | virgile | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | Sulfur-20171101 | OS | - | OS Version | Ubuntu 17.10 |
| Product Version | Frama-C 16-Sulfur | Target Version | - | Fixed in Version | - |
Description :
Running "frama-c -wp remove_copy_cpp.cpp" on the attached program prints an error message "remove_copy_cpp.cpp:4:17: unknown identifier 'i'". When "i" is declared outside the loop, the message disappears.
As a second, more severe issue, Frama-C subsequently ignores the assertion. It prints "[wp] Proved goals: 0 / 0", and terminates successfully with exit code 0. In a larger program, an error message like the above one is likely to be overlooked, and from a reported verification degree of 100%, the user will infer that his program has been fully verified.