2021-01-15 16:30 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001590Frama-CPlug-in > scopepublic2014-03-13 15:57
Assigned Toyakobowski 
PrioritylowSeveritytextReproducibilityhave not tried
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




yakobowski (manager)

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.


yakobowski (manager)

Fix committed to master branch.


yakobowski (manager)

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 Source_changeset_attached => framac master 0918b2c0
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:53 yakobowski Source_changeset_attached => framac stable/neon 0918b2c0
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
+Issue History