Fixed crash in resolution where, after reporting an error, the cases #type and #module were not handled

2 files changed, 39 insertions, 1 deletions

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 8c910959..900c7459 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -1349,3 +1349,27 @@ module TupleEqualitySupport {
   datatype GoodRecord = GoodRecord(set<(int,int)>)

   datatype BadRecord = BadRecord(set<(int, int->bool)>)  // error: this tuple type does not support equality

 }

+

+// ------------------- non-type variable names -------------------

+

+module NonTypeVariableNames {

+  type X = int

+

+  module Y { }

+

+  method M(m: map<real,string>)

+  {

+    assert X == X;  // error (x2): type name used as variable

+    assert Y == Y;  // error (x2): module name used as variable

+    assert X in m;  // error (x2): type name used as variable

+    assert Y in m;  // error (x2): module name used as variable

+  }

+

+  method N(k: int)

+  {

+    assert k == X;  // error (x2): type name used as variable

+    assert k == Y;  // error (x2): module name used as variable

+    X := k;  // error: type name used as variable

+    Y := k;  // error: module name used as variable

+  }

+}

diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect
index ae3e8cbf..481b47e0 100644
--- a/Test/dafny0/ResolutionErrors.dfy.expect
+++ b/Test/dafny0/ResolutionErrors.dfy.expect
@@ -90,6 +90,20 @@ ResolutionErrors.dfy(1329,15): Error: The name Inner ambiguously refers to a typ
 ResolutionErrors.dfy(1339,29): Error: ghost variables are allowed only in specification contexts

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

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

+ResolutionErrors.dfy(1362,11): Error: name of type (X) is used as a variable

+ResolutionErrors.dfy(1362,16): Error: name of type (X) is used as a variable

+ResolutionErrors.dfy(1363,11): Error: name of module (Y) is used as a variable

+ResolutionErrors.dfy(1363,16): Error: name of module (Y) is used as a variable

+ResolutionErrors.dfy(1364,11): Error: name of type (X) is used as a variable

+ResolutionErrors.dfy(1364,13): Error: second argument to "in" must be a set, multiset, or sequence with elements of type #type, or a map with domain #type (instead got map<real, string>)

+ResolutionErrors.dfy(1365,11): Error: name of module (Y) is used as a variable

+ResolutionErrors.dfy(1365,13): Error: second argument to "in" must be a set, multiset, or sequence with elements of type #module, or a map with domain #module (instead got map<real, string>)

+ResolutionErrors.dfy(1370,16): Error: name of type (X) is used as a variable

+ResolutionErrors.dfy(1370,13): Error: arguments must have the same type (got int and #type)

+ResolutionErrors.dfy(1371,16): Error: name of module (Y) is used as a variable

+ResolutionErrors.dfy(1371,13): Error: arguments must have the same type (got int and #module)

+ResolutionErrors.dfy(1372,4): Error: name of type (X) is used as a variable

+ResolutionErrors.dfy(1373,4): Error: name of module (Y) is used as a variable

 ResolutionErrors.dfy(432,2): Error: More than one anonymous constructor

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

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

@@ -182,4 +196,4 @@ ResolutionErrors.dfy(1106,8): Error: new cannot be applied to a trait
 ResolutionErrors.dfy(1127,13): Error: first argument to / must be of numeric type (instead got set<bool>)

 ResolutionErrors.dfy(1134,18): Error: a call to a possibly non-terminating method is allowed only if the calling method is also declared (with 'decreases *') to be possibly non-terminating

 ResolutionErrors.dfy(1149,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating

-184 resolution/type errors detected in ResolutionErrors.dfy

+198 resolution/type errors detected in ResolutionErrors.dfy