Skip to content

Commit

Permalink
VeriFast docs: rename fn to reverse_in_place
Browse files Browse the repository at this point in the history
  • Loading branch information
btj committed Feb 12, 2025
1 parent c941cb1 commit 0f5042e
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions doc/src/tools/verifast.md
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@ programs.

## Verifying `unsafe` functions

Consider, for example, the function `Node::reverse` below that reverses the
Consider, for example, the function `Node::reverse_in_place` below that reverses the
given linked list in-place and returns a pointer to the first node (which
was the originally the last node).

Expand All @@ -59,7 +59,7 @@ pred Nodes(n: *mut Node; nodes: list<*mut Node>) =

impl Node {

unsafe fn reverse(mut n: *mut Node) -> *mut Node
unsafe fn reverse_in_place(mut n: *mut Node) -> *mut Node
//@ req Nodes(n, ?nodes);
//@ ens Nodes(result, reverse(nodes));
//@ on_unwind_ens false;
Expand Down

0 comments on commit 0f5042e

Please sign in to comment.