2021-03-01 05:56 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000689Frama-CPlug-in > Evapublic2014-02-12 16:59
Reportersignoles 
Assigned Tomonate 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
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
+Relationships

-Notes

~0001424

pascal (reporter)

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)

Fix committed to stable/neon branch.
+Notes

-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
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
2013-12-19 01:12 svn Source_changeset_attached => framac master b1ecd87f
2014-02-12 16:54 monate Source_changeset_attached => framac stable/neon b1ecd87f
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
+Issue History