Frama-C Bug Tracking System - Frama-C
View Issue Details
0000090Frama-CPlug-in > slicingpublic2009-05-20 14:132014-02-12 16:53
Assigned Toyakobowski 
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

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.
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 ;-)
2011-10-27 15:43   
Should we close this one ?
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.
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.
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.
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 ( 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