WP confused by pointers to struct

Question

I'm struggling to have WP verify the postcondition of a function that swaps 2 structs.

typedef struct { int x; int y; } pair;

/*@
    requires \valid({p, q});
    assigns *p, *q;
    ensures *p == \old(*q);
    ensures *q == \old(*p);
*/
void swap(pair *p, pair *q);

If I add a few assertions in the body, WP verifies them all except the last one, which is the same as the first one!

void swap(pair *p, pair *q) {
    pair tmp = *p;

    *p = *q;
    //@ assert *p == \at(*q, Pre);

    *q = tmp;
    //@ assert *q == \at(*p, Pre);

    // WP is not sure anymore!
    //@ assert *p == \at(*q, Pre);
}

This happens with Phosphorus-20170501, on both Windows and Ubuntu.

Note that WP succeeds if the function swaps 2 pointers to int, or 2 elements of an array of struct, instead of 2 pointers to struct.

So, what's the matter with pointers to struct?

Answer 1

This is because you didn't specify that p and q cannot point to the same structure, so WP cannot guess that the last assignment cannot modify (*p).

You can do what you want by adding a precondition:

requires \separated(p, q);