Test CO-W+RR+fri-dmb

Executions for behaviour: "0:R0=1 ; 0:R2=1 ; x=1"

Executions for behaviour: "0:R0=0 ; 0:R2=2 ; x=1"

Executions for behaviour: "0:R0=1 ; 0:R2=2 ; x=1"

Executions for behaviour: "0:R0=2 ; 0:R2=2 ; x=1"

Executions for behaviour: "0:R0=0 ; 0:R2=0 ; x=2"

Executions for behaviour: "0:R0=1 ; 0:R2=0 ; x=2"

Executions for behaviour: "0:R0=1 ; 0:R2=1 ; x=2"

Executions for behaviour: "0:R0=1 ; 0:R2=2 ; x=2"

Executions for behaviour: "0:R0=2 ; 0:R2=2 ; x=2"

ARM CO-W+RR+fri-dmb
"Fri DMBsWR Fre Rfe"
Prefetch=
Com=Fr Rf
Orig=Fri DMBsWR Fre Rfe
{
%x0=x;
%x1=x;
}
 P0           | P1           ;
 LDR R0,[%x0] | MOV R0,#2    ;
 MOV R1,#1    | STR R0,[%x1] ;
 STR R1,[%x0] |              ;
 DMB          |              ;
 LDR R2,[%x0] |              ;
exists 0:R0=1 /\ (x=2 /\ (0:R2=0 \/ 0:R2=1 \/ 0:R2=2) \/ x=1 /\ (0:R2=2 \/ 0:R2=1)) \/ 0:R2=2 /\ (0:R0=2 /\ (x=2 \/ x=1) \/ 0:R0=0 /\ x=1) \/ 0:R0=0 /\ 0:R2=0 /\ x=2