AArch64 NT-0B-af
Variant=precise
TTHM=P0:HA
{
x=1;
pte_x=(af:0);
0:X2=x; 0:X4=y;
1:X2=x; 1:X4=y;
}
P0 | P1 ;
MOV W0,#2 | MOV W0,#2 ;
STR W0,[X2] | STR W0,[X4] ;
DMB ST | DMB SY ;
MOV W1,#1 |L0: ;
STR W1,[X4] | LDR W1,[X2] ;
exists (1:X1=0 /\ [y]=2 /\ fault(P1:L0,x,MMU:AccessFlag))