Dafny: fixed bugs in resolution of multi-dimensional arrays

2 files changed, 12 insertions, 1 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index cd531472..8382a525 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -393,7 +393,10 @@ Dafny program verifier finished with 3 verified, 3 errors
 

 -------------------- ResolutionErrors.dfy --------------------

 ResolutionErrors.dfy(10,16): Error: 'decreases *' is not allowed on ghost loops

-1 resolution/type errors detected in ResolutionErrors.dfy

+ResolutionErrors.dfy(23,11): Error: array selection requires an array2 (got array3<T>)

+ResolutionErrors.dfy(24,12): Error: sequence/array selection requires a sequence or array (got array3<T>)

+ResolutionErrors.dfy(25,11): Error: array selection requires an array4 (got array<T>)

+4 resolution/type errors detected in ResolutionErrors.dfy

 

 -------------------- Array.dfy --------------------

 Array.dfy(10,12): Error: assignment may update an array element not in the enclosing method's modifies clause

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index b105a5c0..77a30102 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -16,3 +16,11 @@ method UmmThisIsntGoingToWork()
    assert a[1] == -1;  // ...for then this would incorrectly verify

    b[a[1]] := 0;

 }

+

+method M<T>(a: array3<T>, b: array<T>, m: int, n: int)

+{

+  // the following invalid expressions were once incorrectly resolved:

+  var x := a[m, n];        // error

+  var y := a[m];           // error

+  var z := b[m, n, m, n];  // error

+}