summaryrefslogtreecommitdiff
path: root/Chalice/tests/predicates/aux-info.chalice
diff options
context:
space:
mode:
Diffstat (limited to 'Chalice/tests/predicates/aux-info.chalice')
-rw-r--r--Chalice/tests/predicates/aux-info.chalice33
1 files changed, 0 insertions, 33 deletions
diff --git a/Chalice/tests/predicates/aux-info.chalice b/Chalice/tests/predicates/aux-info.chalice
deleted file mode 100644
index f457c481..00000000
--- a/Chalice/tests/predicates/aux-info.chalice
+++ /dev/null
@@ -1,33 +0,0 @@
-class Cell {
- var value: int;
-
- predicate p { acc(value,1) }
-
- method test()
- requires p && acc(value,2)
- {
- // previously, the following sequence let to negative secondary permission
- // to the field value.
- fold p
- fold p
- call void()
- call void()
- call void2()
-
- unfold p
- var tmp: int := value
- fold p
- // make sure that at this point we can retain information about the field value
- assert tmp == unfolding p in value
- }
-
- method void()
- requires p
- {}
-
- method void2()
- requires p
- ensures p
- {}
-
-}