From ad80221cf26f0a75c534548d6483c3f963b742cd Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Fri, 30 Sep 2011 16:03:43 -0700
Subject: Dafny: fixed bug in translator when LHS of a call was an array
 element or a nat

---
 Dafny/Translator.cs | 17 ++++++++++++++++-
 1 file changed, 16 insertions(+), 1 deletion(-)

(limited to 'Dafny')

diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs
index 3ec3c291..1e400599 100644
--- a/Dafny/Translator.cs
+++ b/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));
     }
-- 
cgit v1.2.3