Moved resolution of BinaryExpr.ResolveOp until the CheckTypeInference phase, where more type information is known

Refactored ConcreteUpdateStatement to no longer inherit from ConcreteSyntaxStatement.
Fixed numerous places where some recursive checks did not reach.

6 files changed, 32 insertions, 15 deletions

diff --git a/Test/VSComp2010/Problem4-Queens.dfy b/Test/VSComp2010/Problem4-Queens.dfy
index 2f21b7a1..2d4111db 100644
--- a/Test/VSComp2010/Problem4-Queens.dfy
+++ b/Test/VSComp2010/Problem4-Queens.dfy
@@ -34,7 +34,7 @@ method Search(N: int) returns (success: bool, board: seq<int>)
               |board| == N &&

               (forall p :: 0 <= p && p < N ==> IsConsistent(board, p));

   ensures !success ==>

-              (forall B ::

+              (forall B: seq<int> ::

                   |B| == N && (forall i :: 0 <= i && i < N ==> 0 <= B[i] && B[i] < N)

                   ==>

                   (exists p :: 0 <= p && p < N && !IsConsistent(B, p)));

@@ -66,7 +66,7 @@ method SearchAux(N: int, boardSoFar: seq<int>) returns (success: bool, newBoard:
               |newBoard| == N &&

               (forall p :: 0 <= p && p < N ==> IsConsistent(newBoard, p));

   ensures !success ==>

-              (forall B ::

+              (forall B: seq<int> ::

                   |B| == N && (forall i :: 0 <= i && i < N ==> 0 <= B[i] && B[i] < N) &&

                   boardSoFar <= B

                   ==>

@@ -84,7 +84,7 @@ method SearchAux(N: int, boardSoFar: seq<int>) returns (success: bool, newBoard:
     var n := 0;

     while (n < N)

       invariant n <= N;

-      invariant (forall B ::

+      invariant (forall B: seq<int> ::

                   // For any board 'B' with 'N' queens, each placed in an existing row

                   |B| == N && (forall i :: 0 <= i && i < N ==> 0 <= B[i] && B[i] < N) &&

                   // ... where 'B' is an extension of 'boardSoFar'

@@ -122,7 +122,7 @@ method SearchAux(N: int, boardSoFar: seq<int>) returns (success: bool, newBoard:
       } else {

         // Since 'n' is not a consistent placement for a queen in column 'pos', there is also

         // no extension of 'candidateBoard' that would make the entire board consistent.

-        assert (forall B ::

+        assert (forall B: seq<int> ::

                   |B| == N && (forall i :: 0 <= i && i < N ==> 0 <= B[i] && B[i] < N) &&

                   candidateBoard <= B

                   ==>

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 0ca8c4f8..d2ddc057 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -357,6 +357,8 @@ ResolutionErrors.dfy(606,10): Error: ghost variables are allowed only in specifi
 ResolutionErrors.dfy(615,17): Error: 'new' is not allowed in ghost contexts

 ResolutionErrors.dfy(617,20): Error: only ghost methods can be called from this context

 ResolutionErrors.dfy(619,8): Error: calls to methods with side-effects are not allowed inside a hint

+ResolutionErrors.dfy(637,21): Error: the type of this expression is underspecified, but it cannot be an arbitrary type.

+ResolutionErrors.dfy(637,21): Error: the type of this expression is underspecified, but it cannot be an arbitrary type.

 ResolutionErrors.dfy(427,2): Error: More than one default constructor

 ResolutionErrors.dfy(48,13): Error: 'this' is not allowed in a 'static' context

 ResolutionErrors.dfy(109,9): Error: ghost variables are allowed only in specification contexts

@@ -429,7 +431,7 @@ ResolutionErrors.dfy(541,7): Error: let-such-that expressions are allowed only i
 ResolutionErrors.dfy(541,20): Error: ghost variables are allowed only in specification contexts

 ResolutionErrors.dfy(543,7): Error: let-such-that expressions are allowed only in ghost contexts

 ResolutionErrors.dfy(544,18): Error: unresolved identifier: w

-89 resolution/type errors detected in ResolutionErrors.dfy

+91 resolution/type errors detected in ResolutionErrors.dfy

 

 -------------------- ParseErrors.dfy --------------------

 ParseErrors.dfy(4,19): error: a chain cannot have more than one != operator

@@ -703,7 +705,7 @@ Basics.dfy(110,16): Error: assertion violation
 Execution trace:

     (0,0): anon0

     (0,0): anon10_Then

-Basics.dfy(129,10): Error: when left-hand sides 0 and 1 may refer to the same location, they must have the same value

+Basics.dfy(129,10): Error: when left-hand sides 0 and 1 may refer to the same location, they must be assigned the same value

 Execution trace:

     (0,0): anon0

     (0,0): anon10_Then

@@ -712,7 +714,7 @@ Execution trace:
     (0,0): anon6

     (0,0): anon12_Then

     (0,0): anon9

-Basics.dfy(143,10): Error: when left-hand sides 0 and 1 refer to the same location, they must have the same value

+Basics.dfy(143,10): Error: when left-hand sides 0 and 1 refer to the same location, they must be assigned the same value

 Execution trace:

     (0,0): anon0

 Basics.dfy(155,19): Error: assertion violation

@@ -743,7 +745,7 @@ Execution trace:
     (0,0): anon13_Then

     (0,0): anon8

     (0,0): anon14_Then

-Basics.dfy(236,10): Error: when left-hand sides 0 and 1 refer to the same location, they must have the same value

+Basics.dfy(235,10): Error: when left-hand sides 0 and 1 refer to the same location, they must be assigned the same value

 Execution trace:

     (0,0): anon0

 

diff --git a/Test/dafny0/Basics.dfy b/Test/dafny0/Basics.dfy
index ccd55fa3..b451cdf1 100644
--- a/Test/dafny0/Basics.dfy
+++ b/Test/dafny0/Basics.dfy
@@ -207,7 +207,6 @@ method m()
 {

   var i: int, j: int;

   i, j := 3, 6;

-  i, i := 3, 3;

 }

 

 method swap(a: array<int>, i: nat, j: nat)

diff --git a/Test/dafny0/Maps.dfy b/Test/dafny0/Maps.dfy
index 1c245952..b23a3750 100644
--- a/Test/dafny0/Maps.dfy
+++ b/Test/dafny0/Maps.dfy
@@ -103,13 +103,13 @@ method m7()
 }

 method m8()

 {

-   var a := map[];

+   var a: map<int,int> := map[];

    assert forall i :: i !in a; // check emptiness

    var i,n := 0, 100;

    while(i < n)

       invariant 0 <= i <= n;

       invariant forall i | i in a :: a[i] == i * i;

-	  invariant forall k :: 0 <= k < i <==> k in a;

+      invariant forall k :: 0 <= k < i <==> k in a;

    {

       a := a[i := i * i];

       i := i + 1;

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 696a583f..60314836 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -626,3 +626,19 @@ module GhostAllocationTests {
   {

   }

 }

+

+// ------------------------- underspecified types ------------------------------

+

+module UnderspecifiedTypes {

+  method M(S: set<int>) {

+    var n, p, T0 :| 12 <= n && n in T0 && 10 <= p && p in T0 && T0 <= S && p % 2 != n % 2;

+    var T1 :| 12 in T1 && T1 <= S;

+    var T2 :| T2 <= S && 12 in T2;

+    var T3 :| 120 in T3;  // error: underspecified type

+    var T3'0: set<int> :| 120 in T3'0;

+    var T3'1: multiset<int> :| 120 in T3'1;

+    var T3'2: map<int,bool> :| 120 in T3'2;

+    var T3'3: seq<int> :| 120 in T3'3;

+    var T4 :| T4 <= S;

+  }

+}

diff --git a/Test/dafny2/StoreAndRetrieve.dfy b/Test/dafny2/StoreAndRetrieve.dfy
index 93bf1812..1cc906f3 100644
--- a/Test/dafny2/StoreAndRetrieve.dfy
+++ b/Test/dafny2/StoreAndRetrieve.dfy
@@ -1,6 +1,6 @@
 abstract module A {

   import L = Library;

-  class {:autocontracts} StoreAndRetrieve<Thing> {

+  class {:autocontracts} StoreAndRetrieve<Thing(==)> {

     ghost var Contents: set<Thing>;

     predicate Valid

     {

@@ -26,7 +26,7 @@ abstract module A {
 }

 

 module B refines A {

-  class StoreAndRetrieve<Thing> {

+  class StoreAndRetrieve<Thing(==)> {

     var arr: seq<Thing>;

     predicate Valid

     {

@@ -52,14 +52,14 @@ module B refines A {
       }

       var k := arr[i];

       ...;

-      var a :| assume Contents == set x | x in a;

+      var a: seq<Thing> :| assume Contents == set x | x in a;

       arr := a;

     }

   }

 }

 

 module C refines B {

-  class StoreAndRetrieve<Thing> {

+  class StoreAndRetrieve<Thing(==)> {

     method Retrieve...

     {

       ...;