diff options
Diffstat (limited to 'Test/test0/Arrays1.bpl')
-rw-r--r-- | Test/test0/Arrays1.bpl | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/Test/test0/Arrays1.bpl b/Test/test0/Arrays1.bpl index 1f4b693c..bc7c89bb 100644 --- a/Test/test0/Arrays1.bpl +++ b/Test/test0/Arrays1.bpl @@ -1,5 +1,4 @@ -// RUN: %boogie -noVerify %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noVerify %s | %OutputCheck %s
var Q: [int,int][int]int;
procedure P()
@@ -10,9 +9,14 @@ procedure P() // 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}
|