Test CoRR1

Executions for behaviour: "1:R1=1 ; 1:R2=1"

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

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

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

ARM CoRR1 ()
"CoRR1"
Prefetch=1:x=T
{
  P0:R5=x ; P0:R2=2 ; x=1 ;
  P1:R5=x ; 
}

P0        | P1           ;
str R2,R5 | ldr R1,R5 ;
          | ldr R2,R5 ;
exists (1:R1=1 /\ 1:R2=1) \/ (1:R1=1 /\ 1:R2=2) \/ (1:R1=2 /\ 1:R2=1) \/ (1:R1=2 /\ 1:R2=2)