summaryrefslogtreecommitdiff
path: root/Test/test0/Arrays1.bpl
diff options
context:
space:
mode:
Diffstat (limited to 'Test/test0/Arrays1.bpl')
-rw-r--r--Test/test0/Arrays1.bpl44
1 files changed, 22 insertions, 22 deletions
diff --git a/Test/test0/Arrays1.bpl b/Test/test0/Arrays1.bpl
index 4e031cb8..0c9f6044 100644
--- a/Test/test0/Arrays1.bpl
+++ b/Test/test0/Arrays1.bpl
@@ -1,22 +1,22 @@
-// RUN: %boogie -noVerify "%s" | %OutputCheck "%s"
-var Q: [int,int][int]int;
-
-procedure P()
-{
- var q: [int]int;
-
- start:
- // here's how to do it:
- q := Q[5,8];
- q[13] := 21;
-
- // CHECK-L: ${CHECKFILE_NAME}(${LINE:+1},11): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: Q
- Q[5,8] := q;
-
- // not like this:
- // CHECK-L: ${CHECKFILE_NAME}(${LINE:+1},15): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: Q
- Q[5,8][13] := 21; // error: the updated array must be an identifier
- return;
-}
-
-// CHECK-L: 2 type checking errors detected in ${CHECKFILE_NAME}
+// RUN: %boogie -noVerify "%s" | %OutputCheck "%s"
+var Q: [int,int][int]int;
+
+procedure P()
+{
+ var q: [int]int;
+
+ start:
+ // here's how to do it:
+ q := Q[5,8];
+ q[13] := 21;
+
+ // CHECK-L: ${CHECKFILE_NAME}(${LINE:+1},11): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: Q
+ Q[5,8] := q;
+
+ // not like this:
+ // CHECK-L: ${CHECKFILE_NAME}(${LINE:+1},15): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: Q
+ Q[5,8][13] := 21; // error: the updated array must be an identifier
+ return;
+}
+
+// CHECK-L: 2 type checking errors detected in ${CHECKFILE_NAME}