Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001430Frama-CPlug-in > reportpublic2013-05-24 17:592013-05-31 11:24
Assigned Tocorrenson 
PlatformOSOS Version
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

-  Notes
yakobowski (manager)
2013-05-24 23:04

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.
Anne (reporter)
2013-05-27 08:30

Yes, maybe a command-line option to chose whether or not to include the properties that no plugin attempted to prove would be nice.
Anne (reporter)
2013-05-31 11:24

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 ?

- 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

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker