2021-03-02 03:17 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000090Frama-CPlug-in > slicingpublic2014-02-12 16:53
Assigned Toyakobowski 
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.
Attached Files

related to 0000690closedyakobowski Slicing does not preserve some ACSL constructs 



monate (reporter)

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.


Anne (reporter)

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 ;-)


Anne (reporter)

Should we close this one ?


yakobowski (manager)

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.


yakobowski (manager)

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.


signoles (manager)

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.


yakobowski (manager)

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
Date Modified Username Field Change
2009-05-20 14:13 Anne New Issue
2009-05-20 14:13 Anne Status new => assigned
2009-05-20 14:13 Anne Assigned To => Anne
2009-05-20 16:02 monate Note Added: 0000080
2009-05-20 16:08 Anne Note Added: 0000081
2009-08-26 11:50 Anne Status assigned => acknowledged
2011-10-27 15:43 Anne Status acknowledged => assigned
2011-10-27 15:43 Anne Assigned To Anne => patrick
2011-10-27 15:43 Anne Note Added: 0002426
2012-01-18 23:39 yakobowski Note Added: 0002586
2012-01-18 23:39 yakobowski Status assigned => closed
2012-01-18 23:39 yakobowski Resolution open => won't fix
2013-01-08 10:29 yakobowski Relationship added related to 0000690
2013-01-08 10:40 yakobowski Note Added: 0003649
2013-01-08 10:40 yakobowski Assigned To patrick => signoles
2013-01-08 10:41 yakobowski Resolution won't fix => reopened
2013-01-08 10:46 yakobowski Status closed => feedback
2013-01-09 16:16 signoles Status feedback => assigned
2013-01-09 16:16 signoles Assigned To signoles => yakobowski
2013-01-09 16:17 signoles Note Added: 0003657
2013-01-19 12:46 yakobowski Note Added: 0003667
2013-01-19 13:05 svn
2013-01-19 13:07 yakobowski Status assigned => resolved
2013-01-19 13:07 yakobowski Resolution reopened => fixed
2013-04-19 11:05 signoles Fixed in Version => Frama-C Fluorine
2013-04-19 11:05 signoles Status resolved => closed
2013-12-19 01:11 yakobowski Source_changeset_attached => framac master bf69de1e
2014-02-12 16:53 yakobowski Source_changeset_attached => framac stable/neon bf69de1e
+Issue History