Skip to content

Commit

Permalink
Fix doc (#1492)
Browse files Browse the repository at this point in the history
* Add test_peek_mut anchor in peek_mut_pledges.rs

* Update panic.md

* Update peek.md
  • Loading branch information
pixelshot91 authored Feb 14, 2024
1 parent c1a5b12 commit 2a4f04c
Show file tree
Hide file tree
Showing 3 changed files with 6 additions and 4 deletions.
4 changes: 2 additions & 2 deletions docs/user-guide/src/tour/peek.md
Original file line number Diff line number Diff line change
Expand Up @@ -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.

<!-- TODO: link capabilities/limitations chapter (refs in structs) -->

Expand All @@ -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}}
```
```
2 changes: 1 addition & 1 deletion docs/user-guide/src/verify/panic.md
Original file line number Diff line number Diff line change
Expand Up @@ -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() {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand All @@ -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
}
}
//// ANCHOR_END: test_peek_mut
}

0 comments on commit 2a4f04c

Please sign in to comment.