Dafny: fix resolution crash (using multi-dimensional arrays in loop alternative)

2 files changed, 49 insertions, 40 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 0723bcba..9a8c7541 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -419,50 +419,50 @@ Execution trace:
 Dafny program verifier finished with 3 verified, 3 errors

 

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

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

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

-ResolutionErrors.dfy(101,9): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')

-ResolutionErrors.dfy(105,11): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(106,9): Error: actual out-parameter 0 is required to be a ghost variable

-ResolutionErrors.dfy(113,15): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(117,23): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(124,4): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(128,21): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(129,35): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(138,9): Error: only ghost methods can be called from this context

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

-ResolutionErrors.dfy(185,27): Error: ghost-context break statement is not allowed to break out of non-ghost structure

-ResolutionErrors.dfy(208,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop

-ResolutionErrors.dfy(220,12): Error: trying to break out of more loop levels than there are enclosing loops

-ResolutionErrors.dfy(224,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop

-ResolutionErrors.dfy(229,8): Error: return statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

+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

+ResolutionErrors.dfy(110,9): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')

+ResolutionErrors.dfy(114,11): Error: ghost variables are allowed only in specification contexts

+ResolutionErrors.dfy(115,9): Error: actual out-parameter 0 is required to be a ghost variable

+ResolutionErrors.dfy(122,15): Error: ghost variables are allowed only in specification contexts

+ResolutionErrors.dfy(126,23): Error: ghost variables are allowed only in specification contexts

+ResolutionErrors.dfy(133,4): Error: ghost variables are allowed only in specification contexts

+ResolutionErrors.dfy(137,21): Error: ghost variables are allowed only in specification contexts

+ResolutionErrors.dfy(138,35): Error: ghost variables are allowed only in specification contexts

+ResolutionErrors.dfy(147,9): Error: only ghost methods can be called from this context

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

+ResolutionErrors.dfy(194,27): Error: ghost-context break statement is not allowed to break out of non-ghost structure

+ResolutionErrors.dfy(217,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop

+ResolutionErrors.dfy(229,12): Error: trying to break out of more loop levels than there are enclosing loops

+ResolutionErrors.dfy(233,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop

+ResolutionErrors.dfy(238,8): Error: return statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

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

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

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

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

-ResolutionErrors.dfy(45,14): Error: a field must be selected via an object, not just a class name

-ResolutionErrors.dfy(46,7): Error: unresolved identifier: F

-ResolutionErrors.dfy(47,14): Error: an instance function must be selected via an object, not just a class name

-ResolutionErrors.dfy(47,7): Error: call to instance function requires an instance

-ResolutionErrors.dfy(48,7): Error: unresolved identifier: G

-ResolutionErrors.dfy(50,7): Error: unresolved identifier: M

-ResolutionErrors.dfy(51,7): Error: call to instance method requires an instance

-ResolutionErrors.dfy(52,7): Error: unresolved identifier: N

-ResolutionErrors.dfy(55,8): Error: non-function expression is called with parameters

-ResolutionErrors.dfy(56,14): Error: member z does not exist in class Global

-ResolutionErrors.dfy(75,12): Error: the name 'Benny' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.Benny')

-ResolutionErrors.dfy(80,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')

-ResolutionErrors.dfy(81,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')

-ResolutionErrors.dfy(83,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')

-ResolutionErrors.dfy(85,12): Error: wrong number of arguments to datatype constructor Abc (found 2, expected 1)

-ResolutionErrors.dfy(247,4): Error: label shadows an enclosing label

-ResolutionErrors.dfy(252,2): Error: duplicate label

-ResolutionErrors.dfy(278,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called

-ResolutionErrors.dfy(279,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called

-ResolutionErrors.dfy(281,4): Error: a constructor is only allowed to be called when an object is being allocated

-ResolutionErrors.dfy(295,16): Error: arguments must have the same type (got int and DTD_List)

-ResolutionErrors.dfy(296,16): Error: arguments must have the same type (got DTD_List and int)

-ResolutionErrors.dfy(297,25): Error: arguments must have the same type (got bool and int)

+ResolutionErrors.dfy(54,14): Error: a field must be selected via an object, not just a class name

+ResolutionErrors.dfy(55,7): Error: unresolved identifier: F

+ResolutionErrors.dfy(56,14): Error: an instance function must be selected via an object, not just a class name

+ResolutionErrors.dfy(56,7): Error: call to instance function requires an instance

+ResolutionErrors.dfy(57,7): Error: unresolved identifier: G

+ResolutionErrors.dfy(59,7): Error: unresolved identifier: M

+ResolutionErrors.dfy(60,7): Error: call to instance method requires an instance

+ResolutionErrors.dfy(61,7): Error: unresolved identifier: N

+ResolutionErrors.dfy(64,8): Error: non-function expression is called with parameters

+ResolutionErrors.dfy(65,14): Error: member z does not exist in class Global

+ResolutionErrors.dfy(84,12): Error: the name 'Benny' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.Benny')

+ResolutionErrors.dfy(89,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')

+ResolutionErrors.dfy(90,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')

+ResolutionErrors.dfy(92,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')

+ResolutionErrors.dfy(94,12): Error: wrong number of arguments to datatype constructor Abc (found 2, expected 1)

+ResolutionErrors.dfy(256,4): Error: label shadows an enclosing label

+ResolutionErrors.dfy(261,2): Error: duplicate label

+ResolutionErrors.dfy(287,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called

+ResolutionErrors.dfy(288,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called

+ResolutionErrors.dfy(290,4): Error: a constructor is only allowed to be called when an object is being allocated

+ResolutionErrors.dfy(304,16): Error: arguments must have the same type (got int and DTD_List)

+ResolutionErrors.dfy(305,16): Error: arguments must have the same type (got DTD_List and int)

+ResolutionErrors.dfy(306,25): Error: arguments must have the same type (got bool and int)

 44 resolution/type errors detected in ResolutionErrors.dfy

 

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

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index f8adaad5..1b68ad91 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -24,6 +24,15 @@ method ManyIndices<T>(a: array3<T>, b: array<T>, m: int, n: int)
   var z := b[m, n, m, n];  // error

 }

 

+method SB(b: array2<int>, s: int) returns (x: int, y: int)

+  requires b != null;

+{

+  while

+  {

+    case b[x,y] == s =>

+  }

+}

+

 // -------- name resolution

 

 class Global {