--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on August 2018 ---
Hi Frama-C community, I'm working on a project using Frama-c (with WP plug-in) and I have some issues related to pointer aliasing. I minimized my problem to the following program: int **a; int *b; /*@ requires \valid(a + (0 .. 9)) && \valid(a[0 .. 9] + (0 .. 9)); @ requires \valid(b + (0 .. 9)); @ requires \separated(a + (0 .. 9), a[0 .. 9] + (0 .. 9), b + (0 .. 9)); @ assigns b[0 .. 1]; @*/ void f(); /*@ requires \valid(a + (0 .. 9)) && \valid(a[0 .. 9] + (0 .. 9)); @ requires \valid(b + (0 .. 9)); @ requires \separated(a + (0 .. 9), a[0 .. 9] + (0 .. 9), b + (0 .. 9)); @ assigns b[0 .. 1]; @*/ void g() { L: f(); //@ assert a[0][0] == \at(a[0][0], L); } Frama-c/WP(Chlorine-20180501) cannot prove the assertion holds. I used provers cvc4, alt-ergo and z3 with 40 seconds time limit and 4000 M memory limit. This program is mainly about pointer aliasing. A function "f" only modifies "b[0 .. 1]" and the assertion states that "a[0][0]" is unchanged before and after a call to "f". I have stated that all pointers are separated so that modifying "b[0 .. 1]" shall not affect "a[0][0]". Why the assertion cannot be proved ? Later, I tried to change the "@assigns b[0 .. 1];" in the contract of function "f" to "@assigns b[0], b[1];", then the assertion can be easily proved. So why are they different ? Thank you, Ziqing Luo University of Delaware -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20180830/b73d7280/attachment.html>