2021-03-05 02:49 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002363Frama-CPlug-in > clangpublic2018-02-12 13:27
Assigned Tovirgile 
PlatformSulfur-20171101OSOS VersionUbuntu 17.10
Product VersionFrama-C 16-Sulfur 
Target VersionFixed in Version 
Summary0002363: variable declared in "for" init-part unrecognized in loop body assigns clause; 100% verification degree reported nevertheless
DescriptionRunning "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.
TagsNo tags attached.
Attached Files


There are no notes attached to this issue.

-Issue History
Date Modified Username Field Change
2018-02-12 13:27 Jochen New Issue
2018-02-12 13:27 Jochen Status new => assigned
2018-02-12 13:27 Jochen Assigned To => virgile
2018-02-12 13:27 Jochen File Added: remove_copy_cpp.cpp
+Issue History