Fix issue 132. The formal argument can't be assume to be allocated when a

function is invoked inside an "Old" expression.

1 files changed, 5 insertions, 2 deletions

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 0314344d..52f52abf 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -5045,8 +5045,11 @@ namespace Microsoft.Dafny {
           CheckSubrange(ee.tok, etran.TrExpr(ee), et, builder);

           Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(p.tok, lhs, CondApplyBox(p.tok, etran.TrExpr(ee), cce.NonNull(ee.Type), et));

           builder.Add(cmd);

-          builder.Add(new Bpl.CommentCmd("assume allocatedness for argument to function"));

-          builder.Add(new Bpl.AssumeCmd(e.Args[i].tok, MkIsAlloc(lhs, et, etran.HeapExpr)));

+          if (!etran.UsesOldHeap) {

+            // the argument can't be assumed to be allocated for the old heap

+            builder.Add(new Bpl.CommentCmd("assume allocatedness for argument to function"));

+            builder.Add(new Bpl.AssumeCmd(e.Args[i].tok, MkIsAlloc(lhs, et, etran.HeapExpr)));

+          }

         }

         // Check that every parameter is available in the state in which the function is invoked; this means checking that it has

         // the right type and is allocated.  These checks usually hold trivially, on account of that the Dafny language only gives