diff options
| -rw-r--r-- | Source/Dafny/Resolver.cs | 7 | ||||
| -rw-r--r-- | Test/dafny4/Bug131.dfy | 11 | ||||
| -rw-r--r-- | Test/dafny4/Bug131.dfy.expect | 2 |
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
|