diff options
Diffstat (limited to 'Chalice/tests/predicates/mutual-dependence.chalice')
-rw-r--r-- | Chalice/tests/predicates/mutual-dependence.chalice | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/Chalice/tests/predicates/mutual-dependence.chalice b/Chalice/tests/predicates/mutual-dependence.chalice new file mode 100644 index 00000000..a0939607 --- /dev/null +++ b/Chalice/tests/predicates/mutual-dependence.chalice @@ -0,0 +1,24 @@ +class Cell {
+ var value: int;
+ var next: Cell;
+
+ predicate p { q }
+ predicate q { acc(value) && acc(next) && (next != null ==> next.p) }
+
+ method test()
+ requires acc(this.*)
+ {
+ value := 1
+ next := null
+ fold q
+ fold p
+ call void()
+ assert unfolding p in unfolding q in value == 1 // ERROR: should not verify
+ }
+
+ method void()
+ requires p
+ ensures p
+ {}
+
+}
|