Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002363Frama-CPlug-in > clangpublic2018-02-12 13:272018-02-12 13:27
ReporterJochen 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
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 Filescpp file icon remove_copy_cpp.cpp [^] (80 bytes) 2018-02-12 13:27

- Relationships

-  Notes
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


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker