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.
|ID0002363||Frama-C||Plug-in > clang||public||2018-02-12||2018-02-12|
|Platform||Sulfur-20171101||OS||-||OS Version||Ubuntu 17.10|
|Product Version||Frama-C 16-Sulfur||Target Version||-||Fixed in Version||-|
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.