Predicate fold/unfold tests with list, lseg

src/test/resources/kinduct/list.vpr

@@ -0,0 +1,168 @@
+
+field val: Int
+field next: Ref
+
+predicate list(r: Ref) {
+    acc(r.val) && acc(r.next) && (r.next != null ==> list(r.next))
+}
+
+method itSum(head: Ref)
+    requires list(head)
+{
+    var cur: Ref
+    cur := head
+    var sum: Int
+    sum := 0
+    while (cur != null)
+    {
+        unfold list(cur)
+        sum := sum + cur.val
+        cur := cur.next
+    }
+}
+
+method itSum2(head: Ref)
+    requires list(head)
+{
+    var cur: Ref
+    cur := head
+    var sum: Int
+    sum := 0
+    while (cur != null)
+    {
+        //:: ExpectedOutput(assignment.failed:insufficient.permission)
+        sum := sum + cur.val
+        cur := cur.next
+    }
+}
+
+method itSum3(head: Ref)
+{
+    var cur: Ref
+    cur := head
+    var sum: Int
+    sum := 0
+    while (cur != null)
+    {
+        //:: ExpectedOutput(unfold.failed:insufficient.permission)
+        unfold list(cur)
+        sum := sum + cur.val
+        cur := cur.next
+    }
+}
+
+method itSum4(head: Ref)
+    requires list(head)
+{
+    var cur: Ref
+    cur := head
+    var sum: Int
+    sum := 0
+    while (cur != null)
+    {
+        unfold list(cur)
+        sum := sum + cur.val
+        cur := cur.next
+    }
+    //:: ExpectedOutput(assert.failed:insufficient.permission)
+    assert list(cur)
+}
+
+predicate lseg(this: Ref, end: Ref) {
+    this != end ==> (acc(this.val, write) && acc(this.next, write) && lseg(this.next, end))
+}
+
+predicate single(end: Ref, nxt: Ref) {
+    acc(end.next) && acc(end.val) && end.next == nxt
+}
+
+method listSumLseg(head: Ref)
+    requires list(head)
+{
+    var cur: Ref
+    cur := head
+    var sum: Int
+    sum := 0
+    fold lseg(head, cur)
+    while (cur != null)
+    {
+        unfold list(cur)
+        sum := sum + cur.val
+        var nxt: Ref
+        nxt := cur.next
+        fold single(cur, nxt)
+        concat(head, cur, nxt)
+        cur := nxt
+    }
+    assert lseg(head, cur)
+}
+
+method listSumLseg2(head: Ref)
+    requires list(head)
+{
+    var cur: Ref
+    cur := head
+    var sum: Int
+    sum := 0
+    fold lseg(head, cur)
+    while (cur != null)
+    {
+        unfold list(cur)
+        sum := sum + cur.val
+        var nxt: Ref
+        nxt := cur.next
+        fold single(cur, nxt)
+        concat(head, cur, nxt)
+        //:: ExpectedOutput(assignment.failed:insufficient.permission)
+        cur := cur.next
+    }
+}
+
+method listSumLseg3(head: Ref)
+    requires list(head)
+{
+    var cur: Ref
+    cur := head
+    var sum: Int
+    sum := 0
+    fold lseg(head, cur)
+    while (cur != null)
+    {
+        unfold list(cur)
+        sum := sum + cur.val
+        var nxt: Ref
+        nxt := cur.next
+        //:: ExpectedOutput(fold.failed:insufficient.permission)
+        fold list(nxt)
+        concat(head, cur, nxt)
+        cur := nxt
+    }
+}
+
+method listSumLseg4(head: Ref)
+    requires list(head)
+{
+    var cur: Ref
+    cur := head
+    var sum: Int
+    sum := 0
+    fold lseg(head, cur)
+    while (cur != null)
+    {
+        unfold list(cur)
+        sum := sum + cur.val
+        var nxt: Ref
+        nxt := cur.next
+        fold single(cur, nxt)
+        concat(head, cur, nxt)
+        //:: ExpectedOutput(call.precondition:insufficient.permission)
+        concat(head, cur, nxt)
+        cur := nxt
+    }
+    assert lseg(head, cur)
+}
+
+method concat(head: Ref, end: Ref, nxt: Ref)
+    requires lseg(head, end)
+    requires single(end, nxt)
+    ensures lseg(head, nxt)