// Otherwise, compare two array elements
// to decide if we need to exchange them.
// R10: address of j-th element
// R11: a[j]
// R12: a[j-1]
R10 := Array;
R10 += R2;
// array base address+j
R11 := *R10;
// R11 := a[j]
R12 := R10;
R13 := 1;
R12 -= R13;
// a+j-1
R12 := *R12;
// R12 := a[j-1]
R3 := R12;
// w := a[j-1]
R3 ?= R11;
// Compare a[j-1] and a[j]
R4 := 5;
// Mask for >=
R4 &= R3;
// Extract > and = signs
R3 := OutExchange;
if R4 goto R3; // if a[j-1] >= a[j] do not perform exchange
// Otherwise, perform exchange
R3 := R10;
R4 := 1;
R3 -= R4;
// R5: address of (j-1)th element
*R3 := R11;
// a[j-1] := a[j]
*R10:= R12;
// a[j] := a[j-1]
// Decreasing j (inner loop)
R3 := 1;
R2 -= R3;
// j := j-1
R4 := LoopInner;
if R3 goto R4; // goto LoopInner
// Increasing i (outer loop)
R3 := 1;
R1 += R3;
// i := i+1
R4 := LoopOuter;
if R3 goto R4; // goto LoopOuter
NOP;
170
11 Programming Languages for Safety-Critical Systems
// to decide if we need to exchange them.
// R10: address of j-th element
// R11: a[j]
// R12: a[j-1]
R10 := Array;
R10 += R2;
// array base address+j
R11 := *R10;
// R11 := a[j]
R12 := R10;
R13 := 1;
R12 -= R13;
// a+j-1
R12 := *R12;
// R12 := a[j-1]
R3 := R12;
// w := a[j-1]
R3 ?= R11;
// Compare a[j-1] and a[j]
R4 := 5;
// Mask for >=
R4 &= R3;
// Extract > and = signs
R3 := OutExchange;
if R4 goto R3; // if a[j-1] >= a[j] do not perform exchange
// Otherwise, perform exchange
R3 := R10;
R4 := 1;
R3 -= R4;
// R5: address of (j-1)th element
*R3 := R11;
// a[j-1] := a[j]
*R10:= R12;
// a[j] := a[j-1]
// Decreasing j (inner loop)
R3 := 1;
R2 -= R3;
// j := j-1
R4 := LoopInner;
if R3 goto R4; // goto LoopInner
// Increasing i (outer loop)
R3 := 1;
R1 += R3;
// i := i+1
R4 := LoopOuter;
if R3 goto R4; // goto LoopOuter
NOP;
170
11 Programming Languages for Safety-Critical Systems
