Executions for behaviour:
"0:R0=0 ; 1:R0=1 ; x=1"
Executions for behaviour:
"0:R0=1 ; 1:R0=1 ; x=1"
Executions for behaviour:
"0:R0=0 ; 1:R0=2 ; x=1"
Executions for behaviour:
"0:R0=1 ; 1:R0=2 ; x=1"
Executions for behaviour:
"0:R0=0 ; 1:R0=2 ; x=2"
Executions for behaviour:
"0:R0=1 ; 1:R0=2 ; x=2"
ARM LB+PPO0518 "PodWW Rfe DpDatadW Rfe PosRR PosRW" Cycle=Rfe PosRR PosRW PodWW Rfe DpDatadW Relax= Safe=Rfe PosRW PosRR Pod*W DpDatadW Prefetch= Com=Rf Rf Orig=PodWW Rfe DpDatadW Rfe PosRR PosRW { %y0=y; %x0=x; %x1=x; %y1=y; } P0 | P1 ; LDR R0,[%y0] | LDR R0,[%x1] ; EOR R1,R0,R0 | LDR R1,[%x1] ; ADD R1,R1,#1 | MOV R2,#2 ; STR R1,[%x0] | STR R2,[%x1] ; | MOV R3,#1 ; | STR R3,[%y1] ; exists 1:R0=2 /\ (0:R0=0 /\ (x=1 \/ x=2) \/ 0:R0=1 /\ (x=2 \/ x=1)) \/ 1:R0=1 /\ x=1 /\ (0:R0=1 \/ 0:R0=0)