Fix issue89. Copy the out param to a local before use it in an anonymous

method that is generated by LetExpr. Change the compiler so that each stmt
writes to its own buffer before add it to the program's buffer so that we can
insert the above mentioned copy instruction before the stmt.

2 files changed, 21 insertions, 0 deletions

diff --git a/Test/dafny4/Bug89.dfy b/Test/dafny4/Bug89.dfy
new file mode 100644
index 00000000..12aec5f4
--- /dev/null
+++ b/Test/dafny4/Bug89.dfy
@@ -0,0 +1,15 @@
+// RUN: %dafny  /compile:3 "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+method F() returns(x:int)

+  ensures x == 6;

+{

+  x := 5;

+  x := (var y := 1; y + x);

+}

+

+method Main()

+{

+  var x := F();

+  print x;

+}
\ No newline at end of file
diff --git a/Test/dafny4/Bug89.dfy.expect b/Test/dafny4/Bug89.dfy.expect
new file mode 100644
index 00000000..5221a5d1
--- /dev/null
+++ b/Test/dafny4/Bug89.dfy.expect
@@ -0,0 +1,6 @@
+

+Dafny program verifier finished with 4 verified, 0 errors

+Program compiled successfully

+Running...

+

+6
\ No newline at end of file