Test C-assign-deref-int

C C-assign-deref-int

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

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

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

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