Test C-assign-deref-addr-int

C C-assign-deref-addr-int

{
int z = 0;
int *v = &z;
}

P0 (int *x, int *y) {
  WRITE_ONCE(*x,1) ;
  smp_wmb();
  WRITE_ONCE(*y,1) ;  
}

P1 (int *y, int **v,int *x) {
  int *r0; int r1; int r2;
  r1 = READ_ONCE(*y) ;
  rcu_assign_pointer(*v,x) ;
  r0 = lockless_dereference(*v) ;
  r2 = READ_ONCE(*r0) ;
}

Observed
    1:r2=0; 1:r1=1; 1:r0=x;