diff options
Diffstat (limited to 'Source/Dafny/Translator.cs')
-rw-r--r-- | Source/Dafny/Translator.cs | 5 |
1 files changed, 2 insertions, 3 deletions
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) {
|