for a pointer int *p, the expression "(p+1)-p" evaluates to 4 in ACSL rather than to 1 (as in C)
ID0002079: This issue was created automatically from Mantis Issue 2079. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002079 | Frama-Clang | Plug-in > wp | public | 2015-02-19 | 2015-03-20 |
| Reporter | Jochen | Assigned To | correnson | Resolution | fixed |
| Priority | urgent | Severity | major | Reproducibility | always |
| Platform | Neon-20140301+dev-STANCE-Jan2015 | OS | - | OS Version | xubuntu-cfe13.10 |
| Product Version | Frama-C Neon-20140301 | Target Version | - | Fixed in Version | - |
Description :
Running "frama-c -wp 463.c" on the attached program, the assertion "(p+1)-p == 4" in line 7 is proven by qed (I didn't succeed finding command-line options to disable qed and let Alt-Ergo decide.) However, compiling and running the program shows that the literally identical assertion in line 8 fails; which is in accordance with the C Standard (e.g. item 9. in sect. 6.5.6 of the C99 Standard 2007 http://www.open-std.org/jtc1/sc22/wg14/www/docs/n1256.pdf , p.95-->83).
When both assertions are changed to "(p+1)-p == 1", Frama-C verification fails (with the goal "false" given to Alt-Ergo; I didn't succeed obtaining an unsimplified version), while compiling and running succeeds.
Tags :
wp