--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on August 2018 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] a simple program that confuses me



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>