From dd65717941251e2be9df829694a42ec4d015bb53 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Tue, 6 Aug 2013 03:52:25 -0700
Subject: Allow calls to side-effect-free ghost methods from expressions

---
 Source/Dafny/Resolver.cs | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

(limited to 'Source/Dafny/Resolver.cs')

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 7db8592d..13c1b984 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -5767,7 +5767,16 @@ namespace Microsoft.Dafny
       } else if (expr is StmtExpr) {
         var e = (StmtExpr)expr;
         int prevErrorCount = ErrorCount;
-        ResolveStatement(e.S, twoState, codeContext);
+        ResolveStatement(e.S, true, codeContext);
+        if (ErrorCount == prevErrorCount) {
+          var r = e.S as UpdateStmt;
+          if (r != null && r.ResolvedStatements.Count == 1) {
+            var call = r.ResolvedStatements[0] as CallStmt;
+            if (call.Method.Mod.Expressions.Count != 0) {
+              Error(call, "calls to methods with side-effects are not allowed inside a statement expression");
+            }
+          }
+        }
         ResolveExpression(e.E, twoState, codeContext);
         Contract.Assert(e.E.Type != null);  // follows from postcondition of ResolveExpression
         expr.Type = e.E.Type;
-- 
cgit v1.2.3