1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18
C CoWW+poonceonce (* * Result: Never * * Test of write-write coherence, that is, whether or not two successive * writes to the same variable are ordered. *) {} P0(int *x) { WRITE_ONCE(*x, 1); WRITE_ONCE(*x, 2); } exists (x=1)