Chalice: Add regression tests for all fixed bugs and separate the tests in 'examples' into "read" examples and general tests.

1 files changed, 37 insertions, 0 deletions

diff --git a/Chalice/tests/regressions/workitem-10194.chalice b/Chalice/tests/regressions/workitem-10194.chalice
new file mode 100644
index 00000000..5828b0bf
--- /dev/null
+++ b/Chalice/tests/regressions/workitem-10194.chalice
@@ -0,0 +1,37 @@
+class Test {
+	var x: int
+	var tk: token<Test.incX>
+	
+	predicate V { acc(x) }
+	
+	method incX()
+		requires V
+		ensures V
+	{
+		unfold V
+		x := x + 1
+		fold V
+	}
+	
+	method joinTk()
+		requires acc(tk) && tk != null && acc(tk.joinable) && tk.joinable
+		requires eval(tk.fork this.incX(), true)
+		ensures V
+		ensures unfolding V in x == old(x) // ERROR: old(x) is not readable (no error here, previously)
+	{
+		join tk
+		assert V
+	}
+
+	method test()
+		requires acc(x) && x == 0
+		requires acc(tk)
+	{
+		fold V
+		fork tklocal := incX()
+		tk := tklocal
+		call joinTk()
+		unfold V
+		assert x == old(x) // this verified previously (without any errors anywhere in the file)
+	}
+}
\ No newline at end of file