Frama-C news and ideas

To content | To menu | To search | Frama-C Home

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;
  t[i++] = 4;
  t[i--] = 5;
  t[i++] = 6;

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[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.