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