Value may be incorrect in presence of several ensures

ID0000689: This issue was created automatically from Mantis Issue 689. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0000689	Frama-C	Plug-in > Eva	public	2011-01-26	2014-02-12

Reporter	signoles	Assigned To	monate	Resolution	fixed
Priority	normal	Severity	major	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Carbon-20101202-beta2	Target Version	-	Fixed in Version	Frama-C Nitrogen-20111001

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.