Test miniMarc03

AArch64 miniMarc03

{
int x =  1 ; (* oldpage *)
int y =  0 ; (* newpage *)
int z; (* spare PTE *)
pte_z = (oa:phy_x) ;
0:X2=x;
1:X2=x; 1:X4=y;
1:X6=pte_x; 1:X8=pte_y;
1:X7=(oa:phy_x,valid:0); (* invalid entry *)
1:X10=z;
2:X2=x;
}

P0          | P1              | P2           ;
            | STR X7,[X6]     | MOV W0,2     ;
            | LSR X3,X2,12    | STR W0,[X2]  ;
            | DSB ISH         |              ;
            | TLBI VAAE1IS,X3 |              ;
            | DSB ISH         |              ;
            | ISB             |              ;
            | LDR W5,[X10]    |              ;
locations[1:X5;y;]
~exists x=2 /\ 1:X5=1 

(*Should be Forbid*)