GitLab

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

---

Id	Project	Category	View	Due Date	Updated
ID0000571	Frama-C	Plug-in > jessie	public	2010-08-24	2010-09-29

Reporter	pascal	Assigned To	pascal	Resolution	no change required
Priority	normal	Severity	major	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Boron-20100401	Target Version	-	Fixed in Version	-

Description :

A shorter example than the previous ones of functions named "search", where Jessie + Alt-ergo emit an unsound result:

/*@ requires 0 < x <= 1000000000 ; ensures \result / 2 > x; / int function1(int x) { return (2x + 1); }

frama-c -jessie t.c

With Frama-C 20100401, Why 2.26, Alt-ergo 0.91, the post-condition is proved, when it is in fact false for all arguments that satisfy the pre-condition.