On arrays vs. pointer, the ACSL way

Some time ago, we saw that in C arrays and pointers have some subtle differences. A facetious colleague just remarked that this is also the case in ACSL especially if you use the \at(e L) construction which basically says that e is supposed to be evaluated in the state when the program reached label L for the last time. For instance let us consider the following function:

int t[10];
void f() {
  int* p = t;
  int i = 4;
 L0:
  t[i++] = 4;
 L1:
  t[i--] = 5;
 L2:
  t[i++] = 6;
  return;
}

Can you decide which of the following assertions hold just before f returns?

1. assert \at(t[\at(i L0)] L1) == 4;
2. assert \at(t L1)[\at(i L0)] == 4;
3. assert \at(p[\at(i L0)] L1) == 4;
4. assert \at(p L1)[\at(i L0)] == 4;

Answers

  /*@ assert \at(t[\at(i L0)] L1) == 4; */

This assertion is true: namely i is equal to 4 in L0 so that we're evaluating t[4] in L1 which is indeed equal to 4.

/*@ assert \at(t L1)[\at(i L0)] == 4; */

This assertion is true but the evaluation is not that simple: according to ACSL's arrays semantics we convert t into a logic array whose cells have the same value as the one of t in the state L1. Then we access the cell number 4 the value of i at L0 that happens to contain 4.

/*@ assert \at(p[\at(i L0)] L1) == 4; */

This assertion is true for the same reason as the first one.

/*@ assert \at(p L1)[\at(i L0)] == 4; */

This assertion is false because the evaluation is slightly different than in the second case: This time we evaluate the pointer p in L1 the offset i in L0 and we dereference the result in the current state where *(p+4) is 6.