diff options
| author |  Unknown <t-alasdo@MSR-RISE-GUEST.redmond.corp.microsoft.com> | 2011-09-30 17:13:14 -0700 |
|---|---|---|
| committer | Unknown <t-alasdo@MSR-RISE-GUEST.redmond.corp.microsoft.com> | 2011-09-30 17:13:14 -0700 |
| commit | 8adf7bbe35df69ab3d0b62dd7bd7dba3c91f6e24 (patch) | |
| tree | 7cb4ade78ab1b20e24e9c763070434c946941207 /Source | |
| parent | 7919efa35cf3d333b933b85313ecf9212c0a4200 (diff) | |
| parent | 98317a65610d0b592d863d70ee73ee7d7f032416 (diff) | |
Merge
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Dafny/Resolver.cs | 30 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 17 |
2 files changed, 34 insertions, 13 deletions
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index b9f5e7e6..54a3de3b 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/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 {
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 3ec3c291..1e400599 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -3652,7 +3652,22 @@ namespace Microsoft.Dafny { }
ProcessCallStmt(s.Tok, s.Receiver, actualReceiver, s.Method, s.Args, bLhss, lhsTypes, builder, locals, etran);
for (int i = 0; i < lhsBuilders.Count; i++) {
- lhsBuilders[i](bLhss[i], builder, etran);
+ var lhs = s.Lhs[i];
+ Type lhsType = null;
+ if (lhs is IdentifierExpr) {
+ lhsType = lhs.Type;
+ } else if (lhs is FieldSelectExpr) {
+ var fse = (FieldSelectExpr)lhs;
+ lhsType = fse.Field.Type;
+ }
+
+ Bpl.Expr bRhs = bLhss[i]; // the RHS (bRhs) of the assignment to the actual call-LHS (lhs) was a LHS (bLhss[i]) in the Boogie call statement
+ if (lhsType != null) {
+ CheckSubrange(lhs.tok, bRhs, lhsType, builder);
+ }
+ bRhs = etran.CondApplyBox(lhs.tok, bRhs, lhs.Type, lhsType);
+
+ lhsBuilders[i](bRhs, builder, etran);
}
builder.Add(CaptureState(s.Tok));
}
|