Frama-C Bug Tracking System - Frama-C
View Issue Details
0001430Frama-CPlug-in > reportpublic2013-05-24 17:592013-05-31 11:24
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

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.
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.
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 ?