| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 0001430 | Frama-C | Plug-in > report | public | 2013-05-24 17:59 | 2013-05-31 11:24 | ||||||||
| Reporter | Anne | ||||||||||||
| Assigned To | correnson | ||||||||||||
| Priority | normal | Severity | minor | Reproducibility | always | ||||||||
| Status | assigned | Resolution | open | ||||||||||
| Product Version | Frama-C Fluorine-20130401 | ||||||||||||
| Target Version | Fixed in Version | ||||||||||||
| Summary | 0001430: RTE are not in 'report' | ||||||||||||
| Description | 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. | ||||||||||||
| Tags | No tags attached. | ||||||||||||
| Attached Files |
| ||||||||||||
 Relationships |
|
 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 ? |
| 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 |