2021-01-15 19:35 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001430Frama-CPlug-in > reportpublic2013-05-31 11:24
ReporterAnne 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
Product VersionFrama-C Fluorine-20130401 
Target VersionFixed in Version 
Summary0001430: RTE are not in 'report'
DescriptionUsing -rte and then -report :
$ frama-c test.c -rte -then -report
the generated assertions are not in the result.

After a value analysis:
$ frama-c test.c -rte -then -val -then -report
they are in the result now.
TagsNo tags attached.
Attached Files

-Relationships
+Relationships

-Notes

~0003890

yakobowski (manager)

Report intentionally does not report properties that no plugin attempted to prove. The goal was to avoid clobbering results with e.g. properties on which no proof was attempted. If this behavior is changed, a command-line option would be nice.

~0003893

Anne (reporter)

Yes, maybe a command-line option to chose whether or not to include the properties that no plugin attempted to prove would be nice.

~0003932

Anne (reporter)

It also mean that after :
$ frama-c test.c -rte -then -val -then -report
the generated assertions that are in dead code are not in the report, right ?
+Notes

-Issue History
Date Modified Username Field Change
2013-05-24 17:59 Anne New Issue
2013-05-24 17:59 Anne Status new => assigned
2013-05-24 17:59 Anne Assigned To => correnson
2013-05-24 23:04 yakobowski Note Added: 0003890
2013-05-27 08:30 Anne Note Added: 0003893
2013-05-31 11:24 Anne Note Added: 0003932
+Issue History