0001430: RTE are not in 'report' - Frama-C Bug Tracking System

Frama-C Bug Tracking System

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

Platform

OS

OS Version

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.

Relationships

Notes
(0003890) 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.

(0003893) 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.

(0003932) 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 - 2019 MantisBT Team