Fix issue 140. Move the initializion of _this before the TAIL_CALL_START label.

3 files changed, 74 insertions, 1 deletions

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index f5f95bd2..d6b2d9ba 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -937,10 +937,10 @@ namespace Microsoft.Dafny {
         Error("Method {0} has no body", wr, m.FullName);

       } else {

         if (m.IsTailRecursive) {

-          Indent(indent, wr); wr.WriteLine("TAIL_CALL_START: ;");

           if (!m.IsStatic) {

             Indent(indent + IndentAmount, wr); wr.WriteLine("var _this = this;");

           }

+          Indent(indent, wr); wr.WriteLine("TAIL_CALL_START: ;");

         }

         Contract.Assert(enclosingMethod == null);

         enclosingMethod = m;

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

+// RUN: %diff "%s.expect" "%t"
+
+class Node<T> {
+  ghost var List: seq<T>;
+  ghost var Repr: set<Node<T>>;
+
+  var data: T;
+  var next: Node<T>;
+
+  predicate Valid()
+    reads this, Repr
+  {
+    this in Repr && null !in Repr &&
+    (next == null ==> List == [data]) &&
+    (next != null ==>
+        next in Repr && next.Repr <= Repr &&
+        this !in next.Repr &&
+        List == [data] + next.List &&
+        next.Valid())
+  }
+
+  constructor (d: T)
+    modifies this
+    ensures Valid() && fresh(Repr - {this})
+    ensures List == [d]
+  {
+    data, next := d, null;
+    List, Repr := [d], {this};
+  }
+
+  constructor InitAsPredecessor(d: T, succ: Node<T>)
+    requires succ != null && succ.Valid() && this !in succ.Repr;
+    modifies this;
+    ensures Valid() && fresh(Repr - {this} - succ.Repr);
+    ensures List == [d] + succ.List;
+  {
+    data, next := d, succ;
+    List := [d] + succ.List;
+    Repr := {this} + succ.Repr;
+  }
+
+  method Prepend(d: T) returns (r: Node<T>)
+    requires Valid()
+    ensures r != null && r.Valid() && fresh(r.Repr - old(Repr))
+    ensures r.List == [d] + List
+  {
+    r := new Node.InitAsPredecessor(d, this);
+  }
+  
+	method Print()
+		requires Valid()
+		decreases |List|
+	{
+		print data;
+		if (next != null) {
+			next.Print();
+		}
+	}
+}
+
+method Main() 
+{
+	var l2 := new Node(2);
+  var l1 := l2.Prepend(1);
+	l1.Print();
+}
diff --git a/Test/dafny4/Bug140.dfy.expect b/Test/dafny4/Bug140.dfy.expect
new file mode 100644
index 00000000..00c7d129
--- /dev/null
+++ b/Test/dafny4/Bug140.dfy.expect
@@ -0,0 +1,6 @@
+

+Dafny program verifier finished with 11 verified, 0 errors

+Program compiled successfully

+Running...

+

+12
\ No newline at end of file