diff --git a/src/test/resources/stack-verification/Gradual Verification - Stack.pdf b/src/test/resources/stack-verification/Gradual Verification - Stack.pdf new file mode 100644 index 00000000..59decd5e Binary files /dev/null and b/src/test/resources/stack-verification/Gradual Verification - Stack.pdf differ diff --git a/src/test/resources/stack-verification/stack.c0 b/src/test/resources/stack-verification/stack.c0 new file mode 100644 index 00000000..a8d04dd9 --- /dev/null +++ b/src/test/resources/stack-verification/stack.c0 @@ -0,0 +1,236 @@ +#use +// List node +struct Node { + int val; + struct Node *next; +}; + +/*@ +predicate segHelper(struct Node *start, struct Node *end) = + (start == end) ? + (true) + : + ( + acc(start->val) && acc(start->next) && + segHelper(start->next, end) + ) ; +@*/ + +/*@ + +predicate seg(struct Node *start) = + segHelper(start, NULL); +@*/ + + +//-------------------------------------------------------------------lemmas +// Lemma: +void appendLemmaLoopBody(struct Node *a, struct Node *b, struct Node *c) + /*@ + requires segHelper(a, b) && + ( (c == NULL) ? + ( true ) + : + ( acc(c->val) && acc(c->next) && + segHelper(c->next, NULL) + ) + ) && + ( (b == c) ? + ( true ) + : + ( + acc(b->val) && acc(b->next) && + segHelper(b->next, c) + ) + ) ; + @*/ + /*@ + ensures segHelper(a, c) && + ( (c == NULL) ? + ( true ) + : + ( acc(c->val) && acc(c->next) && + segHelper(c->next, NULL) + ) + ) ; + @*/ +{ + if (b == c) { + } else if (a == b) { + //@ unfold segHelper(a, b); + //@ fold segHelper(a, c); + } else { + //@ unfold segHelper(a, b); + appendLemmaLoopBody(a->next, b, c); + //@ fold segHelper(a, c); + } +} + +void appendLemmaAfterLoopBody(struct Node *a, struct Node *b, struct Node *c) + /*@ + requires segHelper(a, b) && + ( (c == NULL) ? true : acc(c->val) && acc(c->next) ) && + ( (b == c) ? + ( true ) + : + ( + acc(b->val) && acc(b->next) && + segHelper(b->next, c) + ) + ) ; + @*/ + /*@ + ensures segHelper(a, c) && + ( (c == NULL) ? true : acc(c->val) && acc(c->next) ) ; + @*/ +{ + if (b == c) { + } else if (a == b) { + //@ unfold segHelper(a, b); + //@ fold segHelper(a, c); + } else { + //@ unfold segHelper(a, b); + appendLemmaAfterLoopBody(a->next, b, c); + //@ fold segHelper(a, c); + } +} + + +struct Node *push(struct Node *head, int val) + //@ requires seg(head); + //@ ensures seg(\result); +{ + //@ unfold seg(head); + //@ unfold segHelper(head, NULL); + + if (head == NULL) { + struct Node *n = alloc(struct Node); + n->val = val; + n->next = head; + //@ fold segHelper(n->next, NULL); + //@ fold segHelper(n, NULL); + //@ fold seg(n); + return n; + } else { + struct Node *curr = head; + //@ unfold segHelper(curr->next, NULL); + + //@ fold segHelper(head, curr); + while (curr->next != NULL) + //@ loop_invariant acc(curr->val) && acc(curr->next); + //@ loop_invariant segHelper(head, curr); + //@ loop_invariant (curr->next == NULL) ? (true) : acc(curr->next->next) && acc(curr->next->val) && segHelper(curr->next->next, NULL); + { + + struct Node *prev = curr; + curr = prev->next; + + //@ unfold segHelper(head, prev); + //@ fold segHelper(prev->next, curr); + + if (head == prev) { + } else { + appendLemmaLoopBody(head->next, prev, curr); + } + + //@ fold segHelper(head, curr); + //@ unfold segHelper(curr->next, NULL); + + } + + struct Node *tmp = alloc(struct Node); + tmp->val = val; + tmp->next = curr->next; + curr->next = tmp; + + //@ fold segHelper(tmp->next, NULL); + //@ fold segHelper(curr->next, NULL); + + //@ unfold segHelper(head, curr); + if (head == curr) { + } else { + appendLemmaAfterLoopBody(head->next, curr, NULL); + } + + //@ fold segHelper(head, NULL); + //@ fold seg(head); + return head; + } +} + +int pop(struct Node *head) + //@ requires seg(head); +{ + + //@ unfold seg(head); + //@ unfold segHelper(head, NULL); + + if (head == NULL) { + //@ fold segHelper(head, NULL); + //@ fold seg(head); + return -1; + } else { + + struct Node *curr = head; + //@ unfold segHelper(curr->next, NULL); + + //@ fold segHelper(head, curr); + while (curr->next != NULL && curr->next->next != NULL) + //@ loop_invariant acc(curr->val) && acc(curr->next); + //@ loop_invariant segHelper(head, curr); + //@ loop_invariant (curr->next == NULL) ? (true) : acc(curr->next->next) && acc(curr->next->val) && segHelper(curr->next->next, NULL); + { + + struct Node *prev = curr; + + curr = prev->next; + + //@ unfold segHelper(head, prev); + //@ fold segHelper(prev->next, curr); + + if (head == prev) { + } else { + appendLemmaLoopBody(head->next, prev, curr); + } + + + + //@ fold segHelper(head, curr); + //@ unfold segHelper(curr->next, NULL); + + + } + + curr->next = NULL; + + return 1; + } +} + + + +struct Node *create_list(int val) + //@ requires true; + //@ ensures seg(\result); +{ + struct Node *n = alloc(struct Node); + n->val = val; + n->next = NULL; + //@ fold segHelper(n->next, NULL); + //@ fold segHelper(n, NULL); + //@ fold seg(n); + return n; +} + + + +int main () + //@ requires true; + //@ ensures true; +{ + struct Node *l = create_list(5); + struct Node *l2 = push(l, 1); + //@ assert seg(l2); + pop(l2); + return 1; +} \ No newline at end of file