//@ requires \pointer(a, n, write);
void foo(int *a, int n) {
int half = n/2;
int *b = a + half;
//@ assert \pointer(b - half, half, write);
// becomes assert (\forall* int i=0..half; Perm(b - half + i, write));
// becomes assert (\forall* int i=0..half; Perm({:ptrAdd(ptrAdd(b, -half), i):}, write));
}
The SimplifyNestedQuantifiers pass generates a trigger for the quantifier because -half is independent of i and therefore constant. But since this computation is not lifted out of the trigger (for example into a let expression) this causes viper to crash due to the invalid trigger. Ideally the resulting quantifier looks like this:
\forall* int i = 0..half; (\let int x = ptrAdd(b, -half); Perm({:ptrAdd(x, i):}), write)
In the following program:
The SimplifyNestedQuantifiers pass generates a trigger for the quantifier because
-halfis independent ofiand therefore constant. But since this computation is not lifted out of the trigger (for example into a let expression) this causes viper to crash due to the invalid trigger. Ideally the resulting quantifier looks like this: