diff options
Diffstat (limited to 'Test/test21/ParallelAssignment.bpl')
-rw-r--r-- | Test/test21/ParallelAssignment.bpl | 122 |
1 files changed, 61 insertions, 61 deletions
diff --git a/Test/test21/ParallelAssignment.bpl b/Test/test21/ParallelAssignment.bpl index 6f7c7639..8ff3b1de 100644 --- a/Test/test21/ParallelAssignment.bpl +++ b/Test/test21/ParallelAssignment.bpl @@ -1,62 +1,62 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
-// RUN: %diff "%s.n.expect" "%t"
-// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
-// RUN: %diff "%s.p.expect" "%t"
-// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
-// RUN: %diff "%s.a.expect" "%t"
-// Examples from the Boogie2 language report
-
-type C, D;
-
-var x : int;
-var y : int;
-var z : int;
-var a : [int]int;
-var b : [int][C, D]int;
-
-procedure P(i:int, j:int, m:C, n:D) returns () modifies x, y, a, b; {
- var x1 : int;
- var y1 : int;
-
- x := x+1;
- a[i] := 12;
-
- assert a[i] == 12;
-
- x1 := x;
- y1 := y;
-
- x, y := y, x;
-
- assert x == y1 && y == x1;
- assert x == x1; // error
-
- x, a[i] := x+1, x;
- assert x == y1+1 && a[i] == y1;
-
- b[i][m, n] := 17;
- b[i][m, n], x := a[x], y;
-
- assert b[i][m, n] == a[y1+1];
- assert false; // error
-}
-
-procedure Q() returns () modifies x, y, z; {
-
- x, y, z := 1, 2, 3;
-
- x, y, z := y, z, x;
- x, y, z := y, z, x;
- x, y, z := y, z, x;
-
- assert x == 1 && y == 2 && z == 3;
-
- x, y, z := y+1, z+1, x+1;
- x, y, z := y+1, z+1, x+1;
- x, y, z := y+1, z+1, x+1;
-
- assert x == 4 && y == 5 && z == 6;
-
- assert a[x] == a[y]; // error
-
+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" +// RUN: %diff "%s.n.expect" "%t" +// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" +// RUN: %diff "%s.p.expect" "%t" +// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" +// RUN: %diff "%s.a.expect" "%t" +// Examples from the Boogie2 language report + +type C, D; + +var x : int; +var y : int; +var z : int; +var a : [int]int; +var b : [int][C, D]int; + +procedure P(i:int, j:int, m:C, n:D) returns () modifies x, y, a, b; { + var x1 : int; + var y1 : int; + + x := x+1; + a[i] := 12; + + assert a[i] == 12; + + x1 := x; + y1 := y; + + x, y := y, x; + + assert x == y1 && y == x1; + assert x == x1; // error + + x, a[i] := x+1, x; + assert x == y1+1 && a[i] == y1; + + b[i][m, n] := 17; + b[i][m, n], x := a[x], y; + + assert b[i][m, n] == a[y1+1]; + assert false; // error +} + +procedure Q() returns () modifies x, y, z; { + + x, y, z := 1, 2, 3; + + x, y, z := y, z, x; + x, y, z := y, z, x; + x, y, z := y, z, x; + + assert x == 1 && y == 2 && z == 3; + + x, y, z := y+1, z+1, x+1; + x, y, z := y+1, z+1, x+1; + x, y, z := y+1, z+1, x+1; + + assert x == 4 && y == 5 && z == 6; + + assert a[x] == a[y]; // error + }
\ No newline at end of file |