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