From c5c2c9465a53e4b35a20ad5efe73882dc6a5af34 Mon Sep 17 00:00:00 2001 From: Unknown Date: Sat, 23 Feb 2013 12:07:20 -0800 Subject: removed call forall and * args to calls --- Test/test1/Answer | 10 +++------- Test/test1/CallForallResolve.bpl | 23 ----------------------- Test/test1/EmptyCallArgs.bpl | 11 ----------- Test/test1/runtest.bat | 1 - 4 files changed, 3 insertions(+), 42 deletions(-) delete mode 100644 Test/test1/CallForallResolve.bpl (limited to 'Test/test1') diff --git a/Test/test1/Answer b/Test/test1/Answer index 94bf2d9a..70b7ea80 100644 --- a/Test/test1/Answer +++ b/Test/test1/Answer @@ -107,8 +107,6 @@ UpdateExprTyping.bpl(36,28): Error: right-hand side in map store with wrong type UpdateExprTyping.bpl(38,27): Error: right-hand side in map store with wrong type: ref (expected: int) UpdateExprTyping.bpl(39,27): Error: right-hand side in map store with wrong type: int (expected: ref) 12 type checking errors detected in UpdateExprTyping.bpl -CallForallResolve.bpl(15,2): Error: call forall is allowed only on procedures with no modifies clause: Q -1 type checking errors detected in CallForallResolve.bpl MapsTypeErrors.bpl(26,6): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: m MapsTypeErrors.bpl(32,2): Error: mismatched types in assignment command (cannot assign int to []int) MapsTypeErrors.bpl(33,3): Error: mismatched types in assignment command (cannot assign []int to int) @@ -127,10 +125,8 @@ MapsTypeErrors.bpl(122,4): Error: mismatched types in assignment command (cannot 15 type checking errors detected in MapsTypeErrors.bpl Orderings.bpl(6,19): Error: parent of constant has incompatible type (int instead of C) 1 type checking errors detected in Orderings.bpl -EmptyCallArgs.bpl(15,17): Error: invalid type for argument 0 in call to P: int (expected: bool) -EmptyCallArgs.bpl(26,7): Error: invalid type for out-parameter 0 in call to Q: int (expected: bool) -EmptyCallArgs.bpl(28,7): Error: invalid type for out-parameter 0 in call to Q: int (expected: bool) -3 type checking errors detected in EmptyCallArgs.bpl +EmptyCallArgs.bpl(19,7): Error: invalid type for out-parameter 0 in call to Q: int (expected: bool) +1 type checking errors detected in EmptyCallArgs.bpl FunBody.bpl(6,45): Error: function body with invalid type: bool (expected: int) FunBody.bpl(8,61): Error: function body with invalid type: int (expected: alpha) FunBody.bpl(10,58): Error: function body with invalid type: int (expected: alpha) @@ -163,4 +159,4 @@ IntReal.bpl(32,6): Error: argument type int does not match expected type real IntReal.bpl(33,6): Error: argument type real does not match expected type int IntReal.bpl(45,8): Error: invalid argument types (real and int) to binary operator div IntReal.bpl(46,8): Error: invalid argument types (real and int) to binary operator mod -18 type checking errors detected in IntReal.bpl \ No newline at end of file +18 type checking errors detected in IntReal.bpl diff --git a/Test/test1/CallForallResolve.bpl b/Test/test1/CallForallResolve.bpl deleted file mode 100644 index 374db174..00000000 --- a/Test/test1/CallForallResolve.bpl +++ /dev/null @@ -1,23 +0,0 @@ -procedure P(x: int) returns (y: int); - -procedure CallP() -{ - call forall P(5); // P is allowed here, even if it has out parameters -} - -var global: bool; - -procedure Q(x: int); - modifies global; - -procedure CallQ() -{ - call forall Q(5); // error: P is not allowed here, because it has a modifies clause -} - -procedure R(x: int); - -procedure CallR() -{ - call forall R(5); // no problem that R has no body, though -} diff --git a/Test/test1/EmptyCallArgs.bpl b/Test/test1/EmptyCallArgs.bpl index 18d837a9..31e4b43f 100644 --- a/Test/test1/EmptyCallArgs.bpl +++ b/Test/test1/EmptyCallArgs.bpl @@ -9,13 +9,6 @@ procedure CallP() { var z:C; call z := P(x, y); - call * := P(x, y); - call z := P(*, y); - call z := P(x, *); - call * := P(*, x); // type error - call * := P(x, *); - call z := P(*, *); - call * := P(*, *); } procedure CallQ() { @@ -24,8 +17,4 @@ procedure CallQ() { var z:bool; call x := Q(x, y); // type error - call * := Q(x, y); - call x := Q(*, y); // type error - call x := Q(x, *); - call * := Q(*, y); } \ No newline at end of file diff --git a/Test/test1/runtest.bat b/Test/test1/runtest.bat index 149e6dc9..ccd04355 100644 --- a/Test/test1/runtest.bat +++ b/Test/test1/runtest.bat @@ -12,7 +12,6 @@ rem set BGEXE=mono ..\..\Binaries\Boogie.exe %BGEXE% %* /noVerify Family.bpl %BGEXE% %* /noVerify AttributeTyping.bpl %BGEXE% %* /noVerify UpdateExprTyping.bpl -%BGEXE% %* /noVerify CallForallResolve.bpl %BGEXE% %* /noVerify MapsTypeErrors.bpl %BGEXE% %* /noVerify Orderings.bpl %BGEXE% %* /noVerify EmptyCallArgs.bpl -- cgit v1.2.3