Frama-C Bug Tracking System - Frama-C
View Issue Details
0000689Frama-CPlug-in > Evapublic2011-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

Notes
(0001424)
pascal   
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   
2014-02-12 16:59   
Fix committed to stable/neon branch.

Issue History
2011-01-26 17:50signolesNew Issue
2011-01-26 17:50signolesStatusnew => assigned
2011-01-26 17:50signolesAssigned To => monate
2011-01-26 18:09signolesProduct Version => Frama-C Carbon-20101202-beta2
2011-01-26 21:38pascalNote Added: 0001424
2011-03-30 14:48svn
2011-03-30 14:48svnStatusassigned => resolved
2011-03-30 14:48svnResolutionopen => fixed
2011-10-10 14:13signolesFixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14signolesStatusresolved => closed
2013-12-19 01:12svnSource_changeset_attached => framac master b1ecd87f
2014-02-12 16:54monateSource_changeset_attached => framac stable/neon b1ecd87f
2014-02-12 16:59monateNote Added: 0004817
2014-02-12 16:59monateStatusclosed => resolved
2018-01-12 14:26signolesCategoryPlug-in > value analysis => Plug-in > Eva