# On arrays vs. pointer, the ACSL way

Virgile Prevosto - 31st Jul 2012

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;
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;`

```  /*@ 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` 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`.

Virgile Prevosto
31st Jul 2012