Executions for behaviour: "1:R0=0 ; 1:R1=0 ; x=1"
Executions for behaviour: "1:R0=1 ; 1:R1=0 ; x=1"
Executions for behaviour: "1:R0=2 ; 1:R1=0 ; x=1"
Executions for behaviour: "1:R0=0 ; 1:R1=1 ; x=1"
Executions for behaviour: "1:R0=1 ; 1:R1=1 ; x=1"
Executions for behaviour: "1:R0=2 ; 1:R1=1 ; x=1"
Executions for behaviour: "1:R0=0 ; 1:R1=2 ; x=1"
Executions for behaviour: "1:R0=1 ; 1:R1=2 ; x=1"
Executions for behaviour: "1:R0=2 ; 1:R1=2 ; x=1"
Executions for behaviour: "1:R0=1 ; 1:R1=0 ; x=2"
Executions for behaviour: "1:R0=2 ; 1:R1=0 ; x=2"
Executions for behaviour: "1:R0=2 ; 1:R1=1 ; x=2"
ARM MP+pos+dmb "PosWW Rfe DMBsRR Fre" Cycle=Rfe DMBsRR Fre PosWW Relax= Safe=Rfe Fre PosWW DMBsRR Prefetch= Com=Rf Fr Orig=PosWW Rfe DMBsRR Fre { %x0=x; %x1=x; } P0 | P1 ; MOV R0,#1 | LDR R0,[%x1] ; STR R0,[%x0] | DMB ; MOV R1,#2 | LDR R1,[%x1] ; STR R1,[%x0] | ; Observed 1:R0=0; 1:R1=0; x=1; and 1:R0=1; 1:R1=0; x=1; and 1:R0=2; 1:R1=0; x=1; and 1:R0=0; 1:R1=1; x=1; and 1:R0=1; 1:R1=1; x=1; and 1:R0=2; 1:R1=1; x=1; and 1:R0=0; 1:R1=2; x=1; and 1:R0=1; 1:R1=2; x=1; and 1:R0=2; 1:R1=2; x=1; and 1:R0=1; 1:R1=0; x=2; and 1:R0=2; 1:R1=0; x=2; and 1:R0=2; 1:R1=1; x=2;