Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001590Frama-CPlug-in > scopepublic2014-01-02 16:372014-03-13 15:57
ReporterAnne 
Assigned Toyakobowski 
PrioritylowSeveritytextReproducibilityhave not tried
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Fluorine-20130601 
Target VersionFixed in VersionFrama-C Neon-20140301 
Summary0001590: Feedback from -remove-redundant-alarms
DescriptionIt would be nice to have the list of the removed annotations when -remove-redundant-alarms is used. At the moment, it is a debug message, but I think that it should be a feedback message instead (could be only printed for -scope-verbose 2 for instance).
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0004404)
yakobowski (manager)
2014-01-12 13:09

Seems reasonable.

Please note I would gladly accept a patch that put statuses on proved properties, instead of removing them. This way, the removing would be tracked by the kernel. However, I'm not going to write it myself in the near future.
(0004405)
yakobowski (manager)
2014-01-12 13:34

Fix committed to master branch.
(0004540)
yakobowski (manager)
2014-02-12 16:57

Fix committed to stable/neon branch.

- Issue History
Date Modified Username Field Change
2014-01-02 16:37 Anne New Issue
2014-01-02 16:37 Anne Status new => assigned
2014-01-02 16:37 Anne Assigned To => yakobowski
2014-01-12 13:09 yakobowski Note Added: 0004404
2014-01-12 13:34 yakobowski Note Added: 0004405
2014-01-12 13:34 yakobowski Status assigned => resolved
2014-01-12 13:34 yakobowski Resolution open => fixed
2014-02-12 16:57 yakobowski Note Added: 0004540
2014-03-13 15:56 signoles Fixed in Version => Frama-C Neon-20140301
2014-03-13 15:57 signoles Status resolved => closed


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker