Frama-C Bug Tracking System - Frama-C
View Issue Details
0001430Frama-CPlug-in > reportpublic2013-05-24 17:592013-05-31 11:24
Anne 
correnson 
normalminoralways
assignedopen 
Frama-C Fluorine-20130401 
 
0001430: RTE are not in 'report'
Using -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.
No tags attached.
Issue History
2013-05-24 17:59AnneNew Issue
2013-05-24 17:59AnneStatusnew => assigned
2013-05-24 17:59AnneAssigned To => correnson
2013-05-24 23:04yakobowskiNote Added: 0003890
2013-05-27 08:30AnneNote Added: 0003893
2013-05-31 11:24AnneNote Added: 0003932

Notes
(0003890)
yakobowski   
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.
(0003893)
Anne   
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.
(0003932)
Anne   
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 ?