0000689: Value may be incorrect in presence of several ensures - Frama-C Bug Tracking System

Frama-C Bug Tracking System

View Issue Details [ Jump to Notes ] [ Related Changesets ]

[ Issue History ] [ Print ]

ID

Project

Category

View Status

Date Submitted

Last Update

0000689

Frama-C

Plug-in > Eva

public

2011-01-26 17:50

2014-02-12 16:59

Reporter

signoles

Assigned To

monate

Priority

normal

Severity

major

Reproducibility

always

Status

closed

Resolution

fixed

Platform

OS

OS Version

Product Version

Frama-C Carbon-20101202-beta2

Target Version

Fixed in Version

Frama-C Nitrogen-20111001

Summary

0000689: Value may be incorrect in presence of several ensures

Description

If a function has 1 valid ensure and 1 invalid ensure, the GUI says that both ensures are invalid.

Steps To Reproduce

==== a.c ==== /*@ ensures \result == 0; @ ensures \false; @ */ int f(void) { return 0; } void main(void) { f(); } ============== $ frama-c-gui a.c Then check the property status of both ensures.

Tags

No tags attached.

Relationships

Notes
(0001424) pascal (reporter) 2011-01-26 21:38	Thinking more about it, I am not sure this is incorrectness per se. Because if one "ensures" is invalid, then everytime the execution reaches the end of the function, you have false in as an hypothesis. That is, the other "ensures" may be valid, but it is not wrong to say that it is also invalid. It's still worth fixing.

(0004817) monate (reporter) 2014-02-12 16:59	Fix committed to stable/neon branch.

Issue History
Date Modified	Username	Field	Change
2011-01-26 17:50	signoles	New Issue
2011-01-26 17:50	signoles	Status	new => assigned
2011-01-26 17:50	signoles	Assigned To	=> monate
2011-01-26 18:09	signoles	Product Version	=> Frama-C Carbon-20101202-beta2
2011-01-26 21:38	pascal	Note Added: 0001424
2011-03-30 14:48	svn	Checkin
2011-03-30 14:48	svn	Status	assigned => resolved
2011-03-30 14:48	svn	Resolution	open => fixed
2011-10-10 14:13	signoles	Fixed in Version	=> Frama-C Nitrogen-20111001
2011-10-10 14:14	signoles	Status	resolved => closed
2014-02-12 16:59	monate	Note Added: 0004817
2014-02-12 16:59	monate	Status	closed => resolved
2018-01-12 14:26	signoles	Category	Plug-in > value analysis => Plug-in > Eva

Copyright © 2000 - 2019 MantisBT Team