From 071a2eae55d581e725a0bbd9a032b4c036b4b266 Mon Sep 17 00:00:00 2001
From: stefanheule <unknown>
Date: Thu, 20 Sep 2012 11:01:25 +0200
Subject: Chalice: New regression test case from workitem 10221.

---
 Chalice/tests/regressions/workitem-10221.chalice   | 158 +++++++++++++++++++++
 .../tests/regressions/workitem-10221.output.txt    |   4 +
 2 files changed, 162 insertions(+)
 create mode 100644 Chalice/tests/regressions/workitem-10221.chalice
 create mode 100644 Chalice/tests/regressions/workitem-10221.output.txt

diff --git a/Chalice/tests/regressions/workitem-10221.chalice b/Chalice/tests/regressions/workitem-10221.chalice
new file mode 100644
index 00000000..2a8ae723
--- /dev/null
+++ b/Chalice/tests/regressions/workitem-10221.chalice
@@ -0,0 +1,158 @@
+// In this example, additional unfold/fold pairs make the verification of the last three methods fail.
+
+class Node {
+  var next : Node;
+  var val : int;
+
+  predicate list {
+    acc(next) && acc(val) && (next!=null ==> next.list)
+  }
+  
+  function vals() : seq<int>
+    requires list
+  {
+    unfolding list in (next == null ? [val] : [val] ++ next.vals())
+  }
+
+  function reverse_vals() : seq<int>
+    requires list
+  {
+    unfolding list in (next == null ? [val] : next.reverse_vals() ++ [val])
+  }
+
+  method reverse_in_place() returns (r:Node)
+    requires list;
+    ensures true;
+  {
+    var l : Node := this;
+    r := null;
+
+    var rev : seq<int> := this.reverse_vals();
+    
+    while (l != null) 
+      invariant l!=null ==> l.list;
+      invariant r!=null ==> r.list;
+      invariant rev == (l==null ? nil<int> : l.reverse_vals()) ++ (r==null ? nil<int> : r.vals());
+    { 
+      var y: Node;
+//      if (r != null) {
+//        unfold r.list; fold r.list;
+//      }
+      unfold l.list;
+//      if (l.next != null) {
+//        unfold l.next.list; fold l.next.list;
+//      }
+    
+      y := l.next;
+      l.next := r;
+      r := l;
+      fold r.list;
+      l := y;
+    }
+    assert r.vals() == rev; // should be the post-condition
+  }
+  
+
+   method reverse_in_place_01() returns (r:Node)
+    requires list;
+    ensures true;
+  {
+    var l : Node := this;
+    r := null;
+
+    var rev : seq<int> := this.reverse_vals();
+    
+    while (l != null) 
+      invariant l!=null ==> l.list;
+      invariant r!=null ==> r.list;
+      invariant rev == (l==null ? nil<int> : l.reverse_vals()) ++ (r==null ? nil<int> : r.vals());
+    { 
+      var y: Node;
+//      if (r != null) {
+//        unfold r.list; fold r.list;
+//      }
+      unfold l.list;
+      if (l.next != null) {
+        unfold l.next.list; fold l.next.list;
+      }
+    
+      y := l.next;
+      l.next := r;
+      r := l;
+      fold r.list;
+      l := y;
+    }
+    assert r.vals() == rev; // should be the post-condition
+  }
+  
+   
+
+   method reverse_in_place_10() returns (r:Node)
+    requires list;
+    ensures true;
+  {
+    var l : Node := this;
+    r := null;
+
+    var rev : seq<int> := this.reverse_vals();
+    
+    while (l != null) 
+      invariant l!=null ==> l.list;
+      invariant r!=null ==> r.list;
+      invariant rev == (l==null ? nil<int> : l.reverse_vals()) ++ (r==null ? nil<int> : r.vals());
+    { 
+      var y: Node;
+      if (r != null) {
+        unfold r.list; fold r.list;
+      }
+      unfold l.list;
+//      if (l.next != null) {
+//        unfold l.next.list; fold l.next.list;
+//      }
+    
+      y := l.next;
+      l.next := r;
+      r := l;
+      fold r.list;
+      l := y;
+    }
+    assert r.vals() == rev; // should be the post-condition
+  }
+  
+   
+
+
+   method reverse_in_place_11() returns (r:Node)
+    requires list;
+    ensures true;
+  {
+    var l : Node := this;
+    r := null;
+
+    var rev : seq<int> := this.reverse_vals();
+    
+    while (l != null) 
+      invariant l!=null ==> l.list;
+      invariant r!=null ==> r.list;
+      invariant rev == (l==null ? nil<int> : l.reverse_vals()) ++ (r==null ? nil<int> : r.vals());
+    { 
+      var y: Node;
+      if (r != null) {
+        unfold r.list; fold r.list;
+      }
+      unfold l.list;
+      if (l.next != null) {
+        unfold l.next.list; fold l.next.list;
+      }
+    
+      y := l.next;
+      l.next := r;
+      r := l;
+      fold r.list;
+      l := y;
+    }
+    assert r.vals() == rev; // should be the post-condition
+  }
+  
+   
+}
\ No newline at end of file
diff --git a/Chalice/tests/regressions/workitem-10221.output.txt b/Chalice/tests/regressions/workitem-10221.output.txt
new file mode 100644
index 00000000..e209c3c1
--- /dev/null
+++ b/Chalice/tests/regressions/workitem-10221.output.txt
@@ -0,0 +1,4 @@
+Verification of workitem-10221.chalice using parameters="" 
+
+
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
-- 
cgit v1.2.3