diff options
| author |  qunyanm <unknown> | 2016-02-09 14:24:59 -0800 |
|---|---|---|
| committer | qunyanm <unknown> | 2016-02-09 14:24:59 -0800 |
| commit | 8ee1a3fdb07906ee3858eb602c1823f9c1343b72 (patch) | |
| tree | c703971140a5dc72a1c418d704616ed9d4316449 /Source | |
| parent | 0d08ec191bf3f15ae89dc243877d9295b3004bc6 (diff) | |
Fix issue 131. Instead of crashing, report an error when an undefined member of
a class is referenced.
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Dafny/Resolver.cs | 7 |
1 files changed, 4 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) {
|