Jessie + alt-ergo unsound in presence of division
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.