diff options
| author |  stefanheule <unknown> | 2012-02-25 03:32:02 -0800 |
|---|---|---|
| committer | stefanheule <unknown> | 2012-02-25 03:32:02 -0800 |
| commit | 26c132918015e06305e53f2d57ca769a3b867194 (patch) | |
| tree | 47ebeef7d817c607f93b6a9f414f926514795c7b /Chalice | |
| parent | 2b9a97c7197244afea26bd8fa8f55bd811bf0a2a (diff) | |
Chalice: Test case for negative permission in the secondary mask.
Diffstat (limited to 'Chalice')
| -rw-r--r-- | Chalice/tests/predicates/aux-info.chalice | 33 |
1 files changed, 33 insertions, 0 deletions
diff --git a/Chalice/tests/predicates/aux-info.chalice b/Chalice/tests/predicates/aux-info.chalice new file mode 100644 index 00000000..f457c481 --- /dev/null +++ b/Chalice/tests/predicates/aux-info.chalice @@ -0,0 +1,33 @@ +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
+ {}
+
+}
|