kani/
vec.rs

1// Copyright Kani Contributors
2// SPDX-License-Identifier: Apache-2.0 OR MIT
3use crate::{Arbitrary, any, any_where};
4
5/// Generates an arbitrary vector whose length is at most MAX_LENGTH.
6pub fn any_vec<T, const MAX_LENGTH: usize>() -> Vec<T>
7where
8    T: Arbitrary,
9{
10    let real_length: usize = any_where(|sz| *sz <= MAX_LENGTH);
11    match real_length {
12        0 => vec![],
13        exact if exact == MAX_LENGTH => exact_vec::<T, MAX_LENGTH>(),
14        _ => {
15            let mut any_vec = exact_vec::<T, MAX_LENGTH>();
16            any_vec.truncate(real_length);
17            any_vec.shrink_to_fit();
18            assert!(any_vec.capacity() == any_vec.len());
19            any_vec
20        }
21    }
22}
23
24/// Generates an arbitrary vector that is exactly EXACT_LENGTH long.
25pub fn exact_vec<T, const EXACT_LENGTH: usize>() -> Vec<T>
26where
27    T: Arbitrary,
28{
29    let boxed_array: Box<[T; EXACT_LENGTH]> = Box::new(any());
30    <[T]>::into_vec(boxed_array)
31}
kani/vec.rs

kani/
vec.rs
