From c5e30c266e804d0f7240cc7151dbd78cc5d5a8ca Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 12 May 2014 11:36:52 +0100 Subject: Converted test0/Arrays1.bpl test to OutputCheck style test. --- Test/test0/Answer | 4 ++-- Test/test0/Arrays1.bpl | 8 ++++++-- Test/test0/Arrays1.bpl.expect | 3 --- 3 files changed, 8 insertions(+), 7 deletions(-) delete mode 100644 Test/test0/Arrays1.bpl.expect (limited to 'Test/test0') 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 -- cgit v1.2.3