Frama-C Bug Tracking System - Frama-C
View Issue Details
0000689Frama-CPlug-in > Evapublic2011-01-26 17:502014-02-12 16:59
signoles 
monate 
normalmajoralways
closedfixed 
Frama-C Carbon-20101202-beta2 
Frama-C Nitrogen-20111001 
0000689: Value may be incorrect in presence of several ensures
If a function has 1 valid ensure and 1 invalid ensure, the GUI says that both ensures are invalid.
==== 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.
No tags attached.
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:48svnCheckin
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
2014-02-12 16:59monateNote Added: 0004817
2014-02-12 16:59monateStatusclosed => resolved
2018-01-12 14:26signolesCategoryPlug-in > value analysis => Plug-in > Eva

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.