Test J4

AArch64 J4
 
{
           pte_x=(valid:0,oa:phy_x);
           0:X2=pte_x;
           0:X1=(valid:1,oa:phy_x);
           0:X3=x;
           x=0;
           1:X3=x;
           1:X13=x;
           y=1;
}
 
P0             |  P1;
            | MOV W7, #1;
STR X1,[X2]    | STR W7,[X3]   ;
DSB SY              |   ;
MOV W7, #1     | L0:LDR W4,[X13];
LDR W7,[X3]    |               ;
 
exists (0:X7=1 /\ fault(P1:L0,x,MMU:Translation))