diff options
Diffstat (limited to 'Chalice/tests/regressions/workitem-10221.chalice')
| -rw-r--r-- | Chalice/tests/regressions/workitem-10221.chalice | 158 |
1 files changed, 0 insertions, 158 deletions
diff --git a/Chalice/tests/regressions/workitem-10221.chalice b/Chalice/tests/regressions/workitem-10221.chalice deleted file mode 100644 index 2a8ae723..00000000 --- a/Chalice/tests/regressions/workitem-10221.chalice +++ /dev/null @@ -1,158 +0,0 @@ -// In this example, additional unfold/fold pairs make the verification of the last three methods fail.
-
-class Node {
- var next : Node;
- var val : int;
-
- predicate list {
- acc(next) && acc(val) && (next!=null ==> next.list)
- }
-
- function vals() : seq<int>
- requires list
- {
- unfolding list in (next == null ? [val] : [val] ++ next.vals())
- }
-
- function reverse_vals() : seq<int>
- requires list
- {
- unfolding list in (next == null ? [val] : next.reverse_vals() ++ [val])
- }
-
- method reverse_in_place() returns (r:Node)
- requires list;
- ensures true;
- {
- var l : Node := this;
- r := null;
-
- var rev : seq<int> := this.reverse_vals();
-
- while (l != null)
- invariant l!=null ==> l.list;
- invariant r!=null ==> r.list;
- invariant rev == (l==null ? nil<int> : l.reverse_vals()) ++ (r==null ? nil<int> : r.vals());
- {
- var y: Node;
-// if (r != null) {
-// unfold r.list; fold r.list;
-// }
- unfold l.list;
-// if (l.next != null) {
-// unfold l.next.list; fold l.next.list;
-// }
-
- y := l.next;
- l.next := r;
- r := l;
- fold r.list;
- l := y;
- }
- assert r.vals() == rev; // should be the post-condition
- }
-
-
- method reverse_in_place_01() returns (r:Node)
- requires list;
- ensures true;
- {
- var l : Node := this;
- r := null;
-
- var rev : seq<int> := this.reverse_vals();
-
- while (l != null)
- invariant l!=null ==> l.list;
- invariant r!=null ==> r.list;
- invariant rev == (l==null ? nil<int> : l.reverse_vals()) ++ (r==null ? nil<int> : r.vals());
- {
- var y: Node;
-// if (r != null) {
-// unfold r.list; fold r.list;
-// }
- unfold l.list;
- if (l.next != null) {
- unfold l.next.list; fold l.next.list;
- }
-
- y := l.next;
- l.next := r;
- r := l;
- fold r.list;
- l := y;
- }
- assert r.vals() == rev; // should be the post-condition
- }
-
-
-
- method reverse_in_place_10() returns (r:Node)
- requires list;
- ensures true;
- {
- var l : Node := this;
- r := null;
-
- var rev : seq<int> := this.reverse_vals();
-
- while (l != null)
- invariant l!=null ==> l.list;
- invariant r!=null ==> r.list;
- invariant rev == (l==null ? nil<int> : l.reverse_vals()) ++ (r==null ? nil<int> : r.vals());
- {
- var y: Node;
- if (r != null) {
- unfold r.list; fold r.list;
- }
- unfold l.list;
-// if (l.next != null) {
-// unfold l.next.list; fold l.next.list;
-// }
-
- y := l.next;
- l.next := r;
- r := l;
- fold r.list;
- l := y;
- }
- assert r.vals() == rev; // should be the post-condition
- }
-
-
-
-
- method reverse_in_place_11() returns (r:Node)
- requires list;
- ensures true;
- {
- var l : Node := this;
- r := null;
-
- var rev : seq<int> := this.reverse_vals();
-
- while (l != null)
- invariant l!=null ==> l.list;
- invariant r!=null ==> r.list;
- invariant rev == (l==null ? nil<int> : l.reverse_vals()) ++ (r==null ? nil<int> : r.vals());
- {
- var y: Node;
- if (r != null) {
- unfold r.list; fold r.list;
- }
- unfold l.list;
- if (l.next != null) {
- unfold l.next.list; fold l.next.list;
- }
-
- y := l.next;
- l.next := r;
- r := l;
- fold r.list;
- l := y;
- }
- assert r.vals() == rev; // should be the post-condition
- }
-
-
-}
\ No newline at end of file |