From cb83cf98d04830e986a101246b3a0a7180a06d36 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Thu, 26 May 2011 00:39:27 -0700
Subject: Dafny implementation: removed always-true "allowGhostFeatures"
 parameter

---
 Source/Dafny/Translator.cs | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

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

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index ca19af7b..eb1d1cca 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -2973,7 +2973,7 @@ namespace Microsoft.Dafny {
       } else if (stmt is AssignStmt) {
         AddComment(builder, stmt, "assignment statement");
         AssignStmt s = (AssignStmt)stmt;
-        TrAssignment(stmt.Tok, s.Lhs, s.Rhs, builder, locals, etran);
+        TrAssignment(stmt.Tok, s.Lhs.Resolved, s.Rhs, builder, locals, etran);
       } else if (stmt is VarDecl) {
         AddComment(builder, stmt, "var-declaration statement");
         VarDecl s = (VarDecl)stmt;
@@ -3903,14 +3903,13 @@ namespace Microsoft.Dafny {
     {
       Contract.Requires(tok != null);
       Contract.Requires(lhs != null);
-      // TODO:  Contract.Requires(!(lhs is ConcreteSyntaxExpression));
+      Contract.Requires(!(lhs is ConcreteSyntaxExpression));
       Contract.Requires(rhs != null);
       Contract.Requires(builder != null);
       Contract.Requires(cce.NonNullElements(locals));
       Contract.Requires(etran != null);
       Contract.Requires(predef != null);
 
-      lhs = lhs.Resolved;  // TODO: delete this line and instead bring in the commented-out precondition above
       TrStmt_CheckWellformed(lhs, builder, locals, etran, true);
 
       if (lhs is IdentifierExpr) {
-- 
cgit v1.2.3