Test CO-W+RR+fri-dmb

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

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

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

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

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

Executions for behaviour: "0:R0=2 ; 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=2 ; 0:R2=0 ; x=2"

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

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

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

Executions for behaviour: "0:R0=0 ; 0:R2=2 ; 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=0 /\ 0:R2=0 /\ x=1) \/ (0:R0=0 /\ 0:R2=0 /\ x=2) \/ (0:R0=0 /\ 0:R2=1 /\ x=1) \/ (0:R0=0 /\ 0:R2=1 /\ x=2) \/ (0:R0=0 /\ 0:R2=2 /\ x=1) \/ (0:R0=0 /\ 0:R2=2 /\ x=2) \/ (0:R0=1 /\ 0:R2=0 /\ x=1) \/ (0:R0=1 /\ 0:R2=0 /\ x=2) \/ (0:R0=1 /\ 0:R2=1 /\ x=1) \/ (0:R0=1 /\ 0:R2=1 /\ x=2) \/ (0:R0=1 /\ 0:R2=2 /\ x=1) \/ (0:R0=1 /\ 0:R2=2 /\ x=2) \/ (0:R0=2 /\ 0:R2=0 /\ x=1) \/ (0:R0=2 /\ 0:R2=0 /\ x=2) \/ (0:R0=2 /\ 0:R2=1 /\ x=1) \/ (0:R0=2 /\ 0:R2=1 /\ x=2) \/ (0:R0=2 /\ 0:R2=2 /\ x=1) \/ (0:R0=2 /\ 0:R2=2 /\ x=2)