Skip to content

Commit 5a85f98

Browse files
gebnerCopilot
andcommitted
Use $unfold/$fold antiquotations in recursive_struct.c
Replace hardcoded struct_node__aux_raw_unfold/raw_fold names with the new $unfold(node) and $fold(node) antiquotations. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
1 parent 34e4435 commit 5a85f98

1 file changed

Lines changed: 4 additions & 4 deletions

File tree

test/recursive_struct.c

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -100,12 +100,12 @@ _rec void traverse(_plain node *head)
100100
}
101101
_ghost_stmt(
102102
elim_is_list_nonnull $(head);
103-
struct_node__aux_raw_unfold $(head)
103+
$unfold(node) $(head)
104104
);
105105
node *nx = head->next;
106106
traverse(nx);
107107
_ghost_stmt(
108-
struct_node__aux_raw_fold $(head);
108+
$fold(node) $(head);
109109
Pulse.Lib.Reference.pts_to_not_null $(head);
110110
intro_is_list_cons $(head) (!($(head)))
111111
);
@@ -122,11 +122,11 @@ bool peek_head(_plain node *head, int *out)
122122
}
123123
_ghost_stmt(
124124
elim_is_list_nonnull $(head);
125-
struct_node__aux_raw_unfold $(head)
125+
$unfold(node) $(head)
126126
);
127127
*out = head->data;
128128
_ghost_stmt(
129-
struct_node__aux_raw_fold $(head);
129+
$fold(node) $(head);
130130
Pulse.Lib.Reference.pts_to_not_null $(head);
131131
intro_is_list_cons $(head) (!($(head)))
132132
);

0 commit comments

Comments
 (0)