Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000689Frama-CPlug-in > value analysispublic2011-01-26 17:502014-02-12 16:59
Reportersignoles 
Assigned Tomonate 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Carbon-20101202-beta2 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000689: Value may be incorrect in presence of several ensures
DescriptionIf 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.
TagsNo tags attached.
Attached Files

- 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


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker