This is from Exploring C Semantics and Pointer Provenance:
  https://www.cl.cam.ac.uk/~pes20/cerberus/cerberus-popl2019.pdf

the following test case:
  https://cerberus.cl.cam.ac.uk/cerberus?defacto/provenance_basic_using_uintptr_t_global_yx.c

GCC emits code with different effects for each of the two functions below even when the objects x and y are adjacent to each other: in f(), the call to printf outputs the modified value of y.  In g(), however, it outputs the value of y before modification.

I consider the code in the test case undefined, but a) my understanding from Richard is that the middle-end intentionally doesn't track pointer provenance through integer conversions (and so doesn't necessarily treat this sort of "object hopping" as undefined), and b) the PNVI model outlined in the paper above and expected to be proposed for C2X makes this code valid (the model allows p to take on the provenance of y as a result of the integer <-> pointer casts).

Looking at the dumps, I think (a) is true for this test case in both f() and g().  The different output from g() appears to be due to the x86_64 back performing the assignment *p = 11 only after it has stored the value of y in the register passed to printf.  Other back-ends I've looked at produce the same output from g() as from f().

int y = 2, x = 1;

void f (void)
{
  long ix = (long)&x;
  long iy = (long)&y;

  ix += 4;

  int *p = (int*)ix;
  int *q = (int*)iy;

  if (p == q) {
    *p = 11;
    __builtin_printf ("%i", y);   // prints 11
  }
}

void g (void)
{
  long ix = (long)&x;
  long iy = (long)&y;

  ix += 4;

  int *p = (int*)ix;
  int *q = (int*)iy;

  if (!__builtin_memcmp (&p, &q, sizeof p)) {
    *p = 11;
    __builtin_printf ("%i", y);   // prints 2
  }
}