Fix issue #58. In TrSplitExpr(), add allocatedness for arguments to the inlined

call.

1 files changed, 12 insertions, 0 deletions

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index f3572948..a648bb3a 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -12478,6 +12478,18 @@ namespace Microsoft.Dafny {
               }

             }

 

+            // allocatedness for arguments to the inlined call in body

+            if (typeSpecializedBody is FunctionCallExpr) {

+              FunctionCallExpr e = (FunctionCallExpr)typeSpecializedBody;

+              for (int i = 0; i < e.Args.Count; i++) {

+                Expression ee = e.Args[i];

+                Type t = e.Function.Formals[i].Type;

+                Expr tr_ee = etran.TrExpr(ee);

+                Bpl.Expr wh = GetWhereClause(e.tok, tr_ee, cce.NonNull(ee.Type), etran);

+                if (wh != null) { fargs = Bpl.Expr.And(fargs, wh); }

+              }

+            }

+

             // body

             var trBody = etran.TrExpr(typeSpecializedBody);

             trBody = CondApplyUnbox(trBody.tok, trBody, typeSpecializedResultType, expr.Type);