Fix issue 131. Instead of crashing, report an error when an undefined member of

a class is referenced.

3 files changed, 17 insertions, 3 deletions

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 99b31923..fe31201a 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -7282,7 +7282,7 @@ namespace Microsoft.Dafny
       return rr.Type;

     }

 

-    MemberDecl ResolveMember(IToken tok, Type receiverType, string memberName, out NonProxyType nptype) {

+    MemberDecl ResolveMember(IToken tok, Type receiverType, string memberName, out NonProxyType nptype, bool classMembersOnly = false) {

       Contract.Requires(tok != null);

       Contract.Requires(receiverType != null);

       Contract.Requires(memberName != null);

@@ -7319,7 +7319,7 @@ namespace Microsoft.Dafny
             reporter.Error(MessageSource.Resolver, tok, "{0} {1} does not have an anonymous constructor", kind, ctype.Name);

           } else {

             // search the static members of the enclosing module or its imports

-            if (moduleInfo.StaticMembers.TryGetValue(memberName, out member)) {

+            if (!classMembersOnly && moduleInfo.StaticMembers.TryGetValue(memberName, out member)) {

               Contract.Assert(member.IsStatic); // moduleInfo.StaticMembers is supposed to contain only static members of the module's implicit class _default

               if (member is AmbiguousMemberDecl) {

                 var ambiguousMember = (AmbiguousMemberDecl)member;

@@ -9236,8 +9236,9 @@ namespace Microsoft.Dafny
         }

       } else if (lhs != null) {

         // ----- 4. Look up name in the type of the Lhs

+        bool classMemberOnly = UserDefinedType.DenotesClass(expr.Lhs.Type) == null ? false : true;

         NonProxyType nptype;

-        member = ResolveMember(expr.tok, expr.Lhs.Type, expr.SuffixName, out nptype);

+        member = ResolveMember(expr.tok, expr.Lhs.Type, expr.SuffixName, out nptype, classMemberOnly);

         if (member != null) {

           Expression receiver;

           if (!member.IsStatic) {

diff --git a/Test/dafny4/Bug131.dfy b/Test/dafny4/Bug131.dfy
new file mode 100644
index 00000000..5d01cf59
--- /dev/null
+++ b/Test/dafny4/Bug131.dfy
@@ -0,0 +1,11 @@
+// RUN: %dafny /compile:0 "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+class Cell {

+  method Test(c: Cell) {

+    assert c.F();

+  }

+}

+

+predicate F()

+

diff --git a/Test/dafny4/Bug131.dfy.expect b/Test/dafny4/Bug131.dfy.expect
new file mode 100644
index 00000000..b4c98652
--- /dev/null
+++ b/Test/dafny4/Bug131.dfy.expect
@@ -0,0 +1,2 @@
+Bug131.dfy(6,13): Error: member F does not exist in class Cell

+1 resolution/type errors detected in Bug131.dfy