any_slice_of_array

Function any_slice_of_array 

Source
pub fn any_slice_of_array<T, const LENGTH: usize>(arr: &[T; LENGTH]) -> &[T]
Expand description

Given an array arr of length LENGTH, this function returns a valid slice of arr with non-deterministic start and end points. This is useful in situations where one wants to verify that all possible slices of a given array satisfy some property.

ยงExample:

let arr = [1, 2, 3];
let slice = kani::slice::any_slice_of_array(&arr);
foo(slice); // where foo is a function that takes a slice and verifies a property about it