diff options
| author |  stefanheule <unknown> | 2012-09-20 11:01:25 +0200 |
|---|---|---|
| committer | stefanheule <unknown> | 2012-09-20 11:01:25 +0200 |
| commit | 071a2eae55d581e725a0bbd9a032b4c036b4b266 (patch) | |
| tree | 8d08f7631b878ee3dce4dc9791a7e1141da2daa0 | |
| parent | f9168987b3ad238db82b52188811915e0cc287c8 (diff) | |
Chalice: New regression test case from workitem 10221.
| -rw-r--r-- | Chalice/tests/regressions/workitem-10221.chalice | 158 | ||||
| -rw-r--r-- | Chalice/tests/regressions/workitem-10221.output.txt | 4 |
2 files changed, 162 insertions, 0 deletions
diff --git a/Chalice/tests/regressions/workitem-10221.chalice b/Chalice/tests/regressions/workitem-10221.chalice new file mode 100644 index 00000000..2a8ae723 --- /dev/null +++ b/Chalice/tests/regressions/workitem-10221.chalice @@ -0,0 +1,158 @@ +// 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 diff --git a/Chalice/tests/regressions/workitem-10221.output.txt b/Chalice/tests/regressions/workitem-10221.output.txt new file mode 100644 index 00000000..e209c3c1 --- /dev/null +++ b/Chalice/tests/regressions/workitem-10221.output.txt @@ -0,0 +1,4 @@ +Verification of workitem-10221.chalice using parameters=""
+
+ +Boogie program verifier finished with 0 errors and 0 smoke test warnings
|