Test NT-02-ctrl

AArch64 NT-02-ctrl
TTHM=P1:HA
Variant=precise
{
int x=1; int y;
pte_x=(af:0,valid:0);
0:X2=y;
0:X6=pte_x;
1:X2=y; 1:X4=x;
}
  P0             | P1           ;
MOV X9,#1        | LDR W0,[X2]  ;
LDSET X9,X7,[X6] | DMB LD       ;
LDR X5,[X6]      |L0:           ;
CMP X5,X7        | LDR W1,[X4]  ;
B.EQ Lout        |              ;
MOV W0,#1        |              ;
STR W0,[X2]      |              ;
Lout:            |              ;
exists (0:X5=(oa:PA(x)) /\ 1:X0=1 /\ 1:X1=0 /\ [PTE(x)]=(oa:PA(x)) /\ fault(P1:L0,x,MMU:Translation)) \/ (0:X5=(oa:PA(x), af:0) /\ 1:X0=1 /\ 1:X1=0 /\ [PTE(x)]=(oa:PA(x)) /\ fault(P1:L0,x,MMU:Translation))