removed call forall and * args to calls

4 files changed, 3 insertions, 42 deletions

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