This project is read-only.

Memory model and use of \arrays_disjoint()

Oct 16, 2012 at 4:37 PM
Edited Oct 16, 2012 at 4:49 PM

Consider the code below and the assertions over arrays using \arrays_disjoint and the output of vcc (latest version, Oct 16).

#include <vcc.h>

void foo1() {
  int a[10];
  _(assert \arrays_disjoint(a, 5, a+1, 5))
}

void foo2() {
  int a[10], b[10];

  _(assert \arrays_disjoint(a, 10, b, 10))
}

void foo3() {
  int a[10], b[10];

  _(assert \arrays_disjoint(a+10, 10, b, 10))
}

Verification of foo1 failed. [0,42]

E:\x.c(5,12) : error VC9500: Assertion '\arrays_disjoint(a, 5, a+1, 5)' did not verify.

Verification of foo2 succeeded. [0,02]

Verification of foo3 succeeded. [0,01] 

Verification errors in 1 function(s)Exiting with 3 (1 error(s).)

 

The assertion of foo1() fails as expected,  foo2() succeeds as expected, but why does the assertion in foo3() succeed ? The problem is that b could possibly follow a in the stack (ie. a+10=b) but in any case (whatever the actual memory layout is) vcc should not conclude that the two arrays starting at a+10 and b with length 10 are disjoint.  

I tested other cases and it seems that \arrays_disjoint() only works as expected (for me, that is) only if the pointers respect to the same array.

Thanks,

Eduardo

Oct 19, 2012 at 1:00 AM

Hi Eduardo,

In the VCC memory model, a and b (or more properly, the ghost objects in which the a and b arrays are fields) are different objects. Different objects that are simultaneously valid do not alias, period.

The proof obligations generated by VCC guarantee that this pretense is sound, i.e., that these separate objects can be simulated by a single, flat chunk of memory. You cannot get to elements of b by taking a[27] or something like that, because a[27] is not a valid address.

So you can look at the guaranteed disjointness as a "feature", albeit a useless one.

hope this helps,

ernie