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)