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.