AArch64 NT-12-ctrl
TTHM=P0:HA
Variant=precise
{
pte_x=(af:0);
x=1;
0:X0=x; 0:X4=y;
1:X0=y; 1:X2=pte_x;
}
P0 | P1 ;
LDR W1,[X0] | LDR W1,[X0] ;
CBZ W1,L0 | DMB LD ;
MOV W3,#1 | LDR X3,[X2] ;
STR W3,[X4] | ;
L0: | ;
exists (1:X1=1 /\ 1:X3=(oa:PA(x), af:0))