From f5a4ee5fb54f704387dcfdc7e4ee183d1bbc7876 Mon Sep 17 00:00:00 2001
From: stefanheule <unknown>
Date: Thu, 20 Sep 2012 11:34:50 +0200
Subject: Chalice: New regression tests for fixed workitems 10189 and 10208.

---
 Chalice/tests/regressions/workitem-10189.chalice   | 23 ++++++++++++
 .../tests/regressions/workitem-10189.output.txt    |  4 +++
 Chalice/tests/regressions/workitem-10208.chalice   | 41 ++++++++++++++++++++++
 .../tests/regressions/workitem-10208.output.txt    |  8 +++++
 4 files changed, 76 insertions(+)
 create mode 100644 Chalice/tests/regressions/workitem-10189.chalice
 create mode 100644 Chalice/tests/regressions/workitem-10189.output.txt
 create mode 100644 Chalice/tests/regressions/workitem-10208.chalice
 create mode 100644 Chalice/tests/regressions/workitem-10208.output.txt

diff --git a/Chalice/tests/regressions/workitem-10189.chalice b/Chalice/tests/regressions/workitem-10189.chalice
new file mode 100644
index 00000000..b37b83f2
--- /dev/null
+++ b/Chalice/tests/regressions/workitem-10189.chalice
@@ -0,0 +1,23 @@
+class Node { 
+	var v: int 
+	var next: Node 
+	 
+	predicate V { 
+			 acc(v) 
+		&& acc(next) 
+		&& (next != null ==> next.V) 
+	} 
+
+	unlimited function length(): int 
+		requires rd(V) 
+	{ 1 + unfolding rd(V) in next == null ? 0 : next.length() } 
+	 
+	unlimited function at(i: int): int
+		requires rd(V) 
+		requires i >= 0 
+		requires i < length() // XXXX
+	{
+		unfolding rd(V) in i == 0 ? v : next.at(i - 1)
+		// Precondition at XXX might not hold
+	} 
+}
\ No newline at end of file
diff --git a/Chalice/tests/regressions/workitem-10189.output.txt b/Chalice/tests/regressions/workitem-10189.output.txt
new file mode 100644
index 00000000..96f05468
--- /dev/null
+++ b/Chalice/tests/regressions/workitem-10189.output.txt
@@ -0,0 +1,4 @@
+Verification of workitem-10189.chalice using parameters="" 
+
+
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/regressions/workitem-10208.chalice b/Chalice/tests/regressions/workitem-10208.chalice
new file mode 100644
index 00000000..ae1a7d89
--- /dev/null
+++ b/Chalice/tests/regressions/workitem-10208.chalice
@@ -0,0 +1,41 @@
+class Test {
+  var f1: int;
+  var f2: int;
+
+  predicate valid {
+    acc(f1) && acc(f2) && f1 == f2
+  }
+  
+  method test()
+    requires valid
+  {
+    unfold valid
+    f1 := 2
+    f2 := 2
+    fold valid
+    
+    /* --- not strictly necessary */
+    unfold valid
+    assert f1 == 2
+    fold valid
+    /* --- */
+    
+    call test2()
+    
+    unfold valid
+    assert f1 == 2 // BUG: this should not verify (1)
+    assert false // BUG: this should not verify (2)
+  }
+  
+  method test2()
+    requires valid
+    ensures valid
+    ensures unfolding valid in f1 == 1 // line (1) above verifies also without this postcondition
+  {
+    unfold valid
+    f1 := 1
+    f2 := 1
+    fold valid
+  }
+  
+}
diff --git a/Chalice/tests/regressions/workitem-10208.output.txt b/Chalice/tests/regressions/workitem-10208.output.txt
new file mode 100644
index 00000000..0666393a
--- /dev/null
+++ b/Chalice/tests/regressions/workitem-10208.output.txt
@@ -0,0 +1,8 @@
+Verification of workitem-10208.chalice using parameters="" 
+
+  26.5: Assertion might not hold. The expression at 26.12 might not evaluate to true.
+
+The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification.
+  9.3: The end of method test is unreachable.
+
+Boogie program verifier finished with 1 errors and 1 smoke test warnings
-- 
cgit v1.2.3