#include <stdio.h>

void swap(int * p, int * q)
{                        /*@{}&7c @XPC {@CP {*p = a}    @Eq {wedge} @CP {*q =   b}}*/
   *p += *q;        /*@{}&7c @XPC {@CP {*p = a+b} @Eq {wedge} @CP {*q =   b}}*/
   *q -= *p;        /*@{}&7c @XPC {@CP {*p = a+b} @Eq {wedge} @CP {*q = -a}}*/
   *p += *q;        /*@{}&7c @XPC {@CP {*p = b }     @Eq {wedge} @CP {*q = -a}}*/
   *q = 0 - *q;    /*@{}&7c @XPC {@CP {*p = b}     @Eq {wedge} @CP {*q =   a}}*/
}

int main () {
  int i=4;
  swap( &i, &i );       /*@{}@XPC {Unexpected @B aliasing in @CP {swap}: @CP {*p} and @CP {*q} @BI both refer to @CP {i}}*/
  printf("i = %d\n", i);
  return 0;
}