removed call forall and * args to calls

12 files changed, 8 insertions, 252 deletions

diff --git a/Test/test0/Answer b/Test/test0/Answer
index d71ac997..8c7ce4c7 100644
--- a/Test/test0/Answer
+++ b/Test/test0/Answer
@@ -291,9 +291,8 @@ Orderings.bpl(18,20): Error: the parent of a constant has to be a constant
 4 name resolution errors detected in Orderings.bpl

 BadQuantifier.bpl(3,15): error: invalid QuantifierBody

 1 parse errors detected in BadQuantifier.bpl

-EmptyCallArgs.bpl(31,2): Error: type variable must occur in types of given arguments: a

-EmptyCallArgs.bpl(32,2): Error: type variable must occur in types of given arguments: a

-2 name resolution errors detected in EmptyCallArgs.bpl

+

+Boogie program verifier finished with 0 verified, 0 errors

 ----- SeparateVerification0.bpl

 SeparateVerification0.bpl(13,6): Error: undeclared identifier: y

 1 name resolution errors detected in SeparateVerification0.bpl

diff --git a/Test/test0/EmptyCallArgs.bpl b/Test/test0/EmptyCallArgs.bpl
index eb1c43b7..d45633e9 100644
--- a/Test/test0/EmptyCallArgs.bpl
+++ b/Test/test0/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(*, y);

-  call * := P(x, *);

-  call z := P(*, *);

-  call * := P(*, *);

 }

 

 procedure CallQ() {

@@ -24,10 +17,4 @@ procedure CallQ() {
   var z:bool;

 

   call z := Q(x, y);

-  call * := Q(x, y);

-  call z := Q(*, y);

-  call z := Q(x, *);

-  call * := Q(*, y);

-  call * := Q(x, *);  // problem: type parameter cannot be inferred

-  call * := Q(*, *);  // problem: type parameter cannot be inferred

 }
\ No newline at end of file
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

diff --git a/Test/test2/Answer b/Test/test2/Answer
index 9625c4db..4a7fd32f 100644
--- a/Test/test2/Answer
+++ b/Test/test2/Answer
@@ -424,11 +424,8 @@ FreeCall.bpl(66,5): Error BP5002: A precondition for this call might not hold.
 FreeCall.bpl(14,3): Related location: This is the precondition that might not hold.

 Execution trace:

     FreeCall.bpl(66,5): anon0

-FreeCall.bpl(87,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    FreeCall.bpl(85,5): anon0

 

-Boogie program verifier finished with 8 verified, 5 errors

+Boogie program verifier finished with 7 verified, 4 errors

 

 -------------------- Arrays.bpl /typeEncoding:m --------------------

 Arrays.bpl(46,5): Error BP5003: A postcondition might not hold on this return path.

@@ -462,34 +459,6 @@ Boogie program verifier finished with 0 verified, 1 error
 

 Boogie program verifier finished with 1 verified, 0 errors

 

--------------------- CallForall.bpl --------------------

-CallForall.bpl(17,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    CallForall.bpl(17,3): anon0

-CallForall.bpl(29,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    CallForall.bpl(28,3): anon0

-CallForall.bpl(41,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    CallForall.bpl(40,3): anon0

-CallForall.bpl(47,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    CallForall.bpl(46,3): anon0

-CallForall.bpl(75,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    CallForall.bpl(75,3): anon0

-CallForall.bpl(111,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    CallForall.bpl(109,3): anon0

-CallForall.bpl(118,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    CallForall.bpl(117,3): anon0

-CallForall.bpl(125,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    CallForall.bpl(124,3): anon0

-

-Boogie program verifier finished with 10 verified, 8 errors

-

 -------------------- ContractEvaluationOrder.bpl --------------------

 ContractEvaluationOrder.bpl(8,1): Error BP5003: A postcondition might not hold on this return path.

 ContractEvaluationOrder.bpl(3,3): Related location: This is the postcondition that might not hold.

diff --git a/Test/test2/CallForall.bpl b/Test/test2/CallForall.bpl
deleted file mode 100644
index 98a62103..00000000
--- a/Test/test2/CallForall.bpl
+++ /dev/null
@@ -1,134 +0,0 @@
-function G(int) returns (int);

-axiom (forall x: int :: { G(x) } 0 <= x ==> G(x) == x);

-

-function F(int) returns (int);

-axiom (forall x: int :: { F(G(x)) } 0 <= x ==> F(G(x)) == 5);

-

-procedure Lemma(y: int)

-  requires 0 <= y;

-  ensures F(y) == 5;

-{

-  // proof:

-  assert G(y) == y;

-}

-

-procedure Main0()

-{

-  assert F(2) == 5;  // error: cannot prove this directly, because of the trigger

-}

-

-procedure Main1()

-{

-  call Lemma(2);

-  assert F(2) == 5;

-}

-

-procedure Main2()

-{

-  call Lemma(3);

-  assert F(2) == 5;  // error: Lemma was instantiated the wrong way

-}

-

-procedure Main3()

-{

-  call forall Lemma(*);

-  assert F(2) == 5;

-}

-

-procedure Main4()

-{

-  call forall Lemma(*);

-  assert false;  // error

-}

-

-procedure Main5(z: int)

-{

-  call forall Lemma(*);

-  assert F(z) == 5;  // error: z might be negative

-}

-

-procedure Main6(z: int)

-  requires 0 <= z;

-{

-  call forall Lemma(*);

-  assert F(z) == 5;

-}

-

-// ------------ several parameters

-

-function K(int, int) returns (int);

-axiom (forall x: int, y: int :: { K(G(x), G(y)) } 0 <= x && 0 <= y ==> K(G(x), G(y)) == 25);

-

-procedure MultivarLemma(x: int, y: int)

-  requires 0 <= x;

-  requires 0 <= y;

-  ensures K(x,y) == 25;

-{

-  // proof:

-  assert G(x) == x;

-  assert G(y) == y;

-}

-

-procedure Multi0(x: int, y: int)

-  requires 0 <= x && 0 <= y;

-{

-  assert K(x,y) == 25;  // error

-}

-

-procedure Multi1(x: int, y: int)

-  requires 0 <= x && 0 <= y;

-{

-  call MultivarLemma(x, y);

-  assert K(x,y) == 25;

-}

-

-procedure Multi2(x: int, y: int)

-  requires 0 <= x && 0 <= y;

-{

-  call forall MultivarLemma(x, y);

-  assert K(x,y) == 25;

-}

-

-procedure Multi3(x: int, y: int)

-  requires 0 <= x && 0 <= y;

-{

-  call forall MultivarLemma(*, y);

-  assert K(x,y) == 25;

-}

-

-procedure Multi4(x: int, y: int)

-  requires 0 <= x && 0 <= y;

-{

-  call forall MultivarLemma(x, *);

-  assert K(x,y) == 25;

-}

-

-procedure Multi5(x: int, y: int)

-  requires 0 <= x && 0 <= y;

-{

-  call forall MultivarLemma(2 + 100, *);

-  assert K(102, y) == 25;

-  assert false;  // error

-}

-

-procedure Multi6(x: int, y: int)

-  requires 0 <= x && 0 <= y;

-{

-  call forall MultivarLemma(*, y);

-  assert K(x+2,y+2) == 25;  // error

-}

-

-procedure Multi7(x: int, y: int)

-  requires 0 <= x && 0 <= y;

-{

-  call forall MultivarLemma(x, *);

-  assert K(x+2,y+2) == 25;  // error

-}

-

-procedure Multi8(x: int, y: int)

-  requires 0 <= x && 0 <= y;

-{

-  call forall MultivarLemma(*, *);

-  assert K(x+2,y+2) == 25;  // that's the ticket!

-}

-

diff --git a/Test/test2/FreeCall.bpl b/Test/test2/FreeCall.bpl
index 06eb737e..a873a4e6 100644
--- a/Test/test2/FreeCall.bpl
+++ b/Test/test2/FreeCall.bpl
@@ -80,17 +80,3 @@ procedure FreeCall4()
     free call b := UncallableReturn(-1);

 }

 

-procedure NormalCall5()

-{

-    call forall TestCallForall(*);

-    assert T(true);

-    assert T(false); // error

-}

-

-procedure FreeCall5()

-{

-    free call forall TestCallForall(*);

-    assert T(true);

-    assert T(false);

-    assert false;

-}

diff --git a/Test/test2/runtest.bat b/Test/test2/runtest.bat
index f32bf844..89715252 100644
--- a/Test/test2/runtest.bat
+++ b/Test/test2/runtest.bat
@@ -27,7 +27,7 @@ for %%f in (Arrays.bpl Lambda.bpl TypeEncodingM.bpl ) do (
 echo -------------------- sk_hack.bpl --------------------

 %BGEXE% %* /noinfer sk_hack.bpl

 

-for %%f in (CallForall.bpl ContractEvaluationOrder.bpl) do (

+for %%f in (ContractEvaluationOrder.bpl) do (

   echo.

   echo -------------------- %%f --------------------

   %BGEXE% %* %%f

diff --git a/Test/test20/Answer b/Test/test20/Answer
index fa33507e..5e4481ca 100644
--- a/Test/test20/Answer
+++ b/Test/test20/Answer
@@ -55,8 +55,7 @@ PolyProcs0.bpl(21,30): Error: invalid type for argument 1 in call to FieldAccess
 PolyProcs0.bpl(21,34): Error: invalid type for argument 2 in call to FieldAccess: ref (expected: Field b)

 PolyProcs0.bpl(25,7): Error: invalid type for out-parameter 0 in call to FieldAccess: bool (expected: int)

 PolyProcs0.bpl(26,35): Error: invalid type for argument 2 in call to FieldAccess: ref (expected: Field b)

-PolyProcs0.bpl(41,35): Error: invalid type for argument 1 in call forall to injective: Field int (expected: ref)

-7 type checking errors detected in PolyProcs0.bpl

+6 type checking errors detected in PolyProcs0.bpl

 TypeSynonyms0.bpl(9,5): Error: type synonym could not be resolved because of cycles: Cyclic0 (replacing body with "bool" to continue resolving)

 TypeSynonyms0.bpl(10,5): Error: type synonym could not be resolved because of cycles: Cyclic1 (replacing body with "bool" to continue resolving)

 TypeSynonyms0.bpl(12,5): Error: type synonym could not be resolved because of cycles: AlsoCyclic (replacing body with "bool" to continue resolving)

diff --git a/Test/test20/PolyProcs0.bpl b/Test/test20/PolyProcs0.bpl
index 609f1167..06d4206c 100644
--- a/Test/test20/PolyProcs0.bpl
+++ b/Test/test20/PolyProcs0.bpl
@@ -30,15 +30,4 @@ procedure injective<b>(heap : <a>[ref, Field a]a, obj0 : ref, obj1 : ref, f : Fi
    requires obj0 != obj1;

    ensures heap[obj0, f] != heap[obj1, f];

 

-procedure testCallForall(heap : <a>[ref, Field a]a) {

-  var f1 : Field int; var f2 : Field bool;

-

-  start:

-    call forall injective(heap, *, *, f1);

-    call forall injective(heap, *, *, f2);

-    call forall injective(heap, *, *, *);

-

-    call forall injective(heap, *, f1, *);  // error: wrong argument type

-}

-

 type ref;