diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-09-29 18:33:09 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-09-29 18:33:09 -0700 |
| commit | 8f65d1f0ba1397b57feb11256c0dc344fee465af (patch) | |
| tree | 96776b8947508ac9729c0fb8f9f742bfbc2b41c0 /Dafny | |
| parent | 899d1f3d30abf3343b88c0e4c6e44db130c6345b (diff) | |
Dafny: improved a resolution error message, and fixed a crash in the resolver
Diffstat (limited to 'Dafny')
| -rw-r--r-- | Dafny/Resolver.cs | 30 |
1 files 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 {
|