Skip to content

Commit

Permalink
Fix IntListSeg predicate
Browse files Browse the repository at this point in the history
rems-project/cerberus#494 made this tests fail,
but it wasn't quite phrased correctly anyways. It may need further
changes for more VIP features later, but this should suffice for now.
  • Loading branch information
dc-mak committed Aug 20, 2024
1 parent f6b0137 commit 504ebe1
Showing 1 changed file with 2 additions and 3 deletions.
5 changes: 2 additions & 3 deletions src/example-archive/simple-examples/working/list_preds.h
Original file line number Diff line number Diff line change
Expand Up @@ -25,11 +25,10 @@ datatype seq {

/*@
predicate (datatype seq) IntListSeg(pointer p, pointer tail) {
if (addr_eq(p,tail)) {
if (ptr_eq(p,tail)) {
return Seq_Nil{};
} else {
take H = Owned<struct list_node>(p);
assert (is_null(H.next) || H.next != NULL);
take tl = IntListSeg(H.next, tail);
return (Seq_Cons { val: H.val, next: tl });
}
Expand Down Expand Up @@ -62,4 +61,4 @@ function [rec] (datatype seq) append(datatype seq xs, datatype seq ys) {
// }
// }
// }
// @*/
// @*/

0 comments on commit 504ebe1

Please sign in to comment.