Test CoRR2

Executions for behaviour: "2:R1=1 ; 2:R2=0 ; 3:R1=0 ; 3:R2=0"

Executions for behaviour: "2:R1=2 ; 2:R2=0 ; 3:R1=0 ; 3:R2=0"

Executions for behaviour: "2:R1=0 ; 2:R2=0 ; 3:R1=1 ; 3:R2=0"

Executions for behaviour: "2:R1=0 ; 2:R2=1 ; 3:R1=1 ; 3:R2=0"

Executions for behaviour: "2:R1=1 ; 2:R2=1 ; 3:R1=1 ; 3:R2=0"

Executions for behaviour: "2:R1=2 ; 2:R2=2 ; 3:R1=1 ; 3:R2=0"

Executions for behaviour: "2:R1=0 ; 2:R2=0 ; 3:R1=2 ; 3:R2=0"

Executions for behaviour: "2:R1=0 ; 2:R2=1 ; 3:R1=2 ; 3:R2=0"

Executions for behaviour: "2:R1=1 ; 2:R2=1 ; 3:R1=2 ; 3:R2=0"

Executions for behaviour: "2:R1=2 ; 2:R2=1 ; 3:R1=2 ; 3:R2=0"

Executions for behaviour: "2:R1=1 ; 2:R2=2 ; 3:R1=2 ; 3:R2=0"

Executions for behaviour: "2:R1=2 ; 2:R2=2 ; 3:R1=2 ; 3:R2=0"

Executions for behaviour: "2:R1=1 ; 2:R2=0 ; 3:R1=0 ; 3:R2=1"

Executions for behaviour: "2:R1=2 ; 2:R2=0 ; 3:R1=0 ; 3:R2=1"

Executions for behaviour: "2:R1=1 ; 2:R2=0 ; 3:R1=1 ; 3:R2=1"

Executions for behaviour: "2:R1=2 ; 2:R2=0 ; 3:R1=1 ; 3:R2=1"

Executions for behaviour: "2:R1=2 ; 2:R2=0 ; 3:R1=2 ; 3:R2=1"

Executions for behaviour: "2:R1=2 ; 2:R2=0 ; 3:R1=1 ; 3:R2=2"

Executions for behaviour: "2:R1=1 ; 2:R2=0 ; 3:R1=2 ; 3:R2=2"

Executions for behaviour: "2:R1=2 ; 2:R2=0 ; 3:R1=2 ; 3:R2=2"

ARM CoRR2 ()
"CoRR2"
{
P0:R5=x ; P0:R1=1 ;
P1:R5=x ; P1:R2=2 ;
P2:R5=x ;
P3:R5=x ;
}
P0       |P1       |P2       |P3          ;
str R1,R5|str R2,R5|ldr R1,R5|ldr R1,R5;
         |         |ldr R2,R5|ldr R2,R5;
Observed
    2:R1=1; 2:R2=0; 3:R1=0; 3:R2=0;
and 2:R1=2; 2:R2=0; 3:R1=0; 3:R2=0;
and 2:R1=0; 2:R2=0; 3:R1=1; 3:R2=0;
and 2:R1=0; 2:R2=1; 3:R1=1; 3:R2=0;
and 2:R1=1; 2:R2=1; 3:R1=1; 3:R2=0;
and 2:R1=2; 2:R2=2; 3:R1=1; 3:R2=0;
and 2:R1=0; 2:R2=0; 3:R1=2; 3:R2=0;
and 2:R1=0; 2:R2=1; 3:R1=2; 3:R2=0;
and 2:R1=1; 2:R2=1; 3:R1=2; 3:R2=0;
and 2:R1=2; 2:R2=1; 3:R1=2; 3:R2=0;
and 2:R1=1; 2:R2=2; 3:R1=2; 3:R2=0;
and 2:R1=2; 2:R2=2; 3:R1=2; 3:R2=0;
and 2:R1=1; 2:R2=0; 3:R1=0; 3:R2=1;
and 2:R1=2; 2:R2=0; 3:R1=0; 3:R2=1;
and 2:R1=1; 2:R2=0; 3:R1=1; 3:R2=1;
and 2:R1=2; 2:R2=0; 3:R1=1; 3:R2=1;
and 2:R1=2; 2:R2=0; 3:R1=2; 3:R2=1;
and 2:R1=2; 2:R2=0; 3:R1=1; 3:R2=2;
and 2:R1=1; 2:R2=0; 3:R1=2; 3:R2=2;
and 2:R1=2; 2:R2=0; 3:R1=2; 3:R2=2;