Frama-C Bug Tracking System - Frama-C
View Issue Details
0000090Frama-CPlug-in > slicingpublic2009-05-20 14:132014-02-12 16:53
ReporterAnne 
Assigned Toyakobowski 
PrioritynormalSeverityminorReproducibilityN/A
StatusclosedResolutionfixed 
PlatformOSOS Version
Product Version 
Target VersionFixed in VersionFrama-C Fluorine-20130401 
Summary0000090: Remove generated annotations from slicing results
DescriptionWe should only keep user annotations : generated annotations will be regenerated by the analysis of the new project.
TagsNo tags attached.
related to 0000690closed yakobowski Slicing does not preserve some ACSL constructs 
Attached Files

Notes
(0000080)
monate   
2009-05-20 16:02   
I cannot see why this is a good idea.

The new project may not be analyzed with an annotation generator. I see no reasons to fore anyone to do it.
(0000081)
Anne   
2009-05-20 16:08   
This is related to the new option [-slicing-keep-annotations] added for Dillon after a long discussion (see Patrick or Pascal to have more information on that).

We can do the above processing only if this option is on if you prefer, but it seemed to me that it is a good idea to do it all the time... but I will not fight for that ;-)
(0002426)
Anne   
2011-10-27 15:43   
Should we close this one ?
(0002586)
yakobowski   
2012-01-18 23:39   
Given that more and more plugins are generatint annotations, it is becoming complicated to regenerate them. Thus I'm closing this bug, but feel free to reopen it if someone has a use case.
(0003649)
yakobowski   
2013-01-08 10:40   
There are currently some limitations with annotations that are alarms. In some cases, an annotation remains, but the statement has been removed. Moreover the alarm table of the new project is not synchronized with the kept annotations. Restarting e.g. RTE on the new project results in twice the same annotation.
(0003657)
signoles   
2013-01-09 16:17   
Your friend is:
Alarms.find: code_annotation -> alarm option

Furthermore, when an annotation is removed, so is the corresponding alarm (if any). Should be enough to do what you want right now.
(0003667)
yakobowski   
2013-01-19 12:46   
Alarms, either generated by RTE or Value will be removed. It is too much work to synchronize the alarms table on the (filter.ml created) project generated by Slicing. We would need a lot of dedicated code to re-register the new alarms correctly, and I'm reluctant to do that without a clear need.

Issue History
2009-05-20 14:13AnneNew Issue
2009-05-20 14:13AnneStatusnew => assigned
2009-05-20 14:13AnneAssigned To => Anne
2009-05-20 16:02monateNote Added: 0000080
2009-05-20 16:08AnneNote Added: 0000081
2009-08-26 11:50AnneStatusassigned => acknowledged
2011-10-27 15:43AnneStatusacknowledged => assigned
2011-10-27 15:43AnneAssigned ToAnne => patrick
2011-10-27 15:43AnneNote Added: 0002426
2012-01-18 23:39yakobowskiNote Added: 0002586
2012-01-18 23:39yakobowskiStatusassigned => closed
2012-01-18 23:39yakobowskiResolutionopen => won't fix
2013-01-08 10:29yakobowskiRelationship addedrelated to 0000690
2013-01-08 10:40yakobowskiNote Added: 0003649
2013-01-08 10:40yakobowskiAssigned Topatrick => signoles
2013-01-08 10:41yakobowskiResolutionwon't fix => reopened
2013-01-08 10:46yakobowskiStatusclosed => feedback
2013-01-09 16:16signolesStatusfeedback => assigned
2013-01-09 16:16signolesAssigned Tosignoles => yakobowski
2013-01-09 16:17signolesNote Added: 0003657
2013-01-19 12:46yakobowskiNote Added: 0003667
2013-01-19 13:05svn
2013-01-19 13:07yakobowskiStatusassigned => resolved
2013-01-19 13:07yakobowskiResolutionreopened => fixed
2013-04-19 11:05signolesFixed in Version => Frama-C Fluorine
2013-04-19 11:05signolesStatusresolved => closed
2013-12-19 01:11yakobowskiSource_changeset_attached => framac master bf69de1e
2014-02-12 16:53yakobowskiSource_changeset_attached => framac stable/neon bf69de1e