From 8f65d1f0ba1397b57feb11256c0dc344fee465af Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Thu, 29 Sep 2011 18:33:09 -0700
Subject: Dafny: improved a resolution error message, and fixed a crash in the
 resolver

---
 Dafny/Resolver.cs | 30 ++++++++++++++++++------------
 1 file changed, 18 insertions(+), 12 deletions(-)

diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs
index b9f5e7e6..54a3de3b 100644
--- a/Dafny/Resolver.cs
+++ b/Dafny/Resolver.cs
@@ -2809,15 +2809,17 @@ namespace Microsoft.Dafny {
 
       } else if (expr is FunctionCallExpr) {
         var e = (FunctionCallExpr)expr;
-        if (e.Function != null && e.Function.IsGhost) {
-          Error(expr, "function calls are allowed only in specification contexts (consider declaring the function a 'function method')");
-          return;
-        }
-        // function is okay, so check all NON-ghost arguments
-        CheckIsNonGhost(e.Receiver);
-        for (int i = 0; i < e.Function.Formals.Count; i++) {
-          if (!e.Function.Formals[i].IsGhost) {
-            CheckIsNonGhost(e.Args[i]);
+        if (e.Function != null) {
+          if (e.Function.IsGhost) {
+            Error(expr, "function calls are allowed only in specification contexts (consider declaring the function a 'function method')");
+            return;
+          }
+          // function is okay, so check all NON-ghost arguments
+          CheckIsNonGhost(e.Receiver);
+          for (int i = 0; i < e.Function.Formals.Count; i++) {
+            if (!e.Function.Formals[i].IsGhost) {
+              CheckIsNonGhost(e.Args[i]);
+            }
           }
         }
         return;
@@ -2885,9 +2887,13 @@ namespace Microsoft.Dafny {
 #endif
       if (member == null) {
         // error has already been reported by ResolveMember
-      } else if (allowMethodCall && member is Method) {
-        // it's a method
-        return new CallRhs(e.tok, e.Receiver, e.Name, e.Args);
+      } else if (member is Method) {
+        if (allowMethodCall) {
+          // it's a method
+          return new CallRhs(e.tok, e.Receiver, e.Name, e.Args);
+        } else {
+          Error(e, "member {0} in type {1} refers to a method, but only functions can be used in this context", e.Name, cce.NonNull(ctype).Name);
+        }
       } else if (!(member is Function)) {
         Error(e, "member {0} in type {1} does not refer to a function", e.Name, cce.NonNull(ctype).Name);
       } else {
-- 
cgit v1.2.3