From 2a4f04c30949e06d9d03c814e66b28e0e3e1a59e Mon Sep 17 00:00:00 2001 From: pixelshot91 Date: Wed, 14 Feb 2024 10:47:11 +0100 Subject: [PATCH] Fix doc (#1492) * Add test_peek_mut anchor in peek_mut_pledges.rs * Update panic.md * Update peek.md --- docs/user-guide/src/tour/peek.md | 4 ++-- docs/user-guide/src/verify/panic.md | 2 +- prusti-tests/tests/verify/pass/user-guide/peek_mut_pledges.rs | 4 +++- 3 files changed, 6 insertions(+), 4 deletions(-) diff --git a/docs/user-guide/src/tour/peek.md b/docs/user-guide/src/tour/peek.md index 19bccb4e764..b997b77106b 100644 --- a/docs/user-guide/src/tour/peek.md +++ b/docs/user-guide/src/tour/peek.md @@ -3,7 +3,7 @@ > **Recommended reading:** > [3.3: Peek](https://rust-unofficial.github.io/too-many-lists/second-peek.html) -Ideally, we could implement `peek` and `try_peek` like we implemented `pop` and `try_pop` before. Like `pop`, `push` can only be called if the list is non-empty, and it then always returns a reference to the element at the head of the list (type `&T`). Similarly, `try_peek` can be called on any list, but returns an `Option<&T>`. The latter is currently not possible in Prusti, since structures containing references are not supported at the moment. +Ideally, we could implement `peek` and `try_peek` like we implemented `pop` and `try_pop` before. Like `pop`, `peek` can only be called if the list is non-empty, and it then always returns a reference to the element at the head of the list (type `&T`). Similarly, `try_peek` can be called on any list, but returns an `Option<&T>`. The latter is currently not possible in Prusti, since structures containing references are not supported at the moment. @@ -27,4 +27,4 @@ Here you can see the full code we have now: ```rust,noplaypen // Expand to see full code up to this chapter {{#rustdoc_include ../../../../prusti-tests/tests/verify/pass/user-guide/peek.rs:nothing}} -``` \ No newline at end of file +``` diff --git a/docs/user-guide/src/verify/panic.md b/docs/user-guide/src/verify/panic.md index c93970d88eb..b2d12fc4683 100644 --- a/docs/user-guide/src/verify/panic.md +++ b/docs/user-guide/src/verify/panic.md @@ -22,7 +22,7 @@ error[P0004]: unreachable!(..) statement might be reachable This message correctly points out that the `unreachable!()` statement might actually be reachable. The message says "might" because Prusti is conservative, i.e., it reports a verification error *unless* it can prove that the statement is unreachable. -Hence, Prusti successfully the example below as it can rule out that the condition in the conditional statement, `a <= 0`, holds. +Hence, Prusti successfully verified the example below as it can rule out that the condition in the conditional statement, `a <= 0`, holds. ```rust,noplaypen,ignore pub fn main() { diff --git a/prusti-tests/tests/verify/pass/user-guide/peek_mut_pledges.rs b/prusti-tests/tests/verify/pass/user-guide/peek_mut_pledges.rs index e083b676514..659eae96dcf 100644 --- a/prusti-tests/tests/verify/pass/user-guide/peek_mut_pledges.rs +++ b/prusti-tests/tests/verify/pass/user-guide/peek_mut_pledges.rs @@ -218,6 +218,7 @@ mod prusti_tests { prusti_assert!(*list.peek() == 16); } + //// ANCHOR: test_peek_mut fn _test_peek_mut() { let mut list = List::new(); list.push(8); @@ -238,4 +239,5 @@ mod prusti_tests { prusti_assert!(*list.lookup(0) == 5); // slot 0 is now `5` prusti_assert!(*list.lookup(1) == 8); // slot 1 is unchanged } -} \ No newline at end of file + //// ANCHOR_END: test_peek_mut +}