Test J3

AArch64 J3
 
{
       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;

STR X1,[X2]    | LDR W7,[X3]   ;
DSB SY              | ;
MOV W7, #1     | L0:LDR W4,[X13];
STR W7,[X3]    |               ;
 
exists (1:X7=1 /\ fault(P1:L0,x,MMU:Translation))