From 2b7d31bb3e0276028a8bc50c4933ea60fed5fb60 Mon Sep 17 00:00:00 2001
From: qunyanm <unknown>
Date: Wed, 4 Nov 2015 10:36:54 -0800
Subject: 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.

---
 Test/dafny4/Bug89.dfy        | 15 +++++++++++++++
 Test/dafny4/Bug89.dfy.expect |  6 ++++++
 2 files changed, 21 insertions(+)
 create mode 100644 Test/dafny4/Bug89.dfy
 create mode 100644 Test/dafny4/Bug89.dfy.expect

(limited to 'Test/dafny4')

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
-- 
cgit v1.2.3