Skip to content

Commit

Permalink
kani::any() can generate arrays
Browse files Browse the repository at this point in the history
There's no need for `from_fn`.
  • Loading branch information
listochkin committed Dec 13, 2024
1 parent 5fc5d8d commit a942282
Show file tree
Hide file tree
Showing 2 changed files with 4 additions and 4 deletions.
6 changes: 3 additions & 3 deletions exercise-book/src/kani-linked-list.md
Original file line number Diff line number Diff line change
Expand Up @@ -396,15 +396,15 @@ mod proofs {
<p>
<details>
<summary>
Generating a list of random elements.
Generating a linked list of random elements.
</summary>

You can make a list by making an array first using [`from_fn`](https://doc.rust-lang.org/std/array/fn.from_fn.html) function.
You can make a list by making an array first using `kani::any()`.
Then you can pass the array to a [`from_iter`](https://doc.rust-lang.org/std/iter/trait.FromIterator.html#tymethod.from_iter) method.

```rust ignore
const TOTAL: usize = 10;
let items: [u32; TOTAL] = std::array::from_fn(|_| kani::any::<u32>());
let items: [u32; TOTAL] = kani::any();

let mut list = DoublyLinkedList::from_iter(items.iter().copied());
assert_eq!(list.len(), TOTAL);
Expand Down
2 changes: 1 addition & 1 deletion exercise-solutions/kani-linked-list/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -284,7 +284,7 @@ mod proofs {
#[cfg_attr(not(rust_analyzer), kani::unwind(20))]
fn remove_at() {
const TOTAL: usize = 10;
let items: [u32; TOTAL] = std::array::from_fn(|_| kani::any::<u32>());
let items: [u32; TOTAL] = kani::any();

let mut list = DoublyLinkedList::from_iter(items.iter().copied());
assert_eq!(list.len(), TOTAL);
Expand Down

0 comments on commit a942282

Please sign in to comment.