diff options
| author |  Dan Liew <daniel.liew@imperial.ac.uk> | 2014-05-12 11:36:52 +0100 |
|---|---|---|
| committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2014-05-12 11:36:52 +0100 |
| commit | c5e30c266e804d0f7240cc7151dbd78cc5d5a8ca (patch) | |
| tree | a1299a125cd74ab84453018afa004c809e956916 | |
| parent | eb2bc55a8b41c79fc856f235c5d333c82f79883e (diff) | |
Converted test0/Arrays1.bpl test to OutputCheck style test.
| -rw-r--r-- | Test/test0/Answer | 4 | ||||
| -rw-r--r-- | Test/test0/Arrays1.bpl | 8 | ||||
| -rw-r--r-- | Test/test0/Arrays1.bpl.expect | 3 |
3 files changed, 8 insertions, 7 deletions
diff --git a/Test/test0/Answer b/Test/test0/Answer index 51798f57..06f85659 100644 --- a/Test/test0/Answer +++ b/Test/test0/Answer @@ -120,8 +120,8 @@ axiom (forall x: int :: {:xname "hello"} {:weight 5} {:ValueFunc f(x + 1)} { f(x Boogie program verifier finished with 0 verified, 0 errors
Boogie program verifier finished with 0 verified, 0 errors
-Arrays1.bpl(13,11): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: Q
-Arrays1.bpl(16,15): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: Q
+Arrays1.bpl(14,11): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: Q
+Arrays1.bpl(18,15): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: Q
2 type checking errors detected in Arrays1.bpl
Types0.bpl(8,18): error: expected identifier before ':'
Types0.bpl(8,12): error: expecting an identifier as parameter name
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}
diff --git a/Test/test0/Arrays1.bpl.expect b/Test/test0/Arrays1.bpl.expect deleted file mode 100644 index 534096ac..00000000 --- a/Test/test0/Arrays1.bpl.expect +++ /dev/null @@ -1,3 +0,0 @@ -Arrays1.bpl(13,11): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: Q -Arrays1.bpl(16,15): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: Q -2 type checking errors detected in Arrays1.bpl |