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.
|ID0002079||Frama-Clang||Plug-in > wp||public||2015-02-19||2015-03-20|
|Product Version||Frama-C Neon-20140301||Target Version||-||Fixed in Version||-|
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.