Function kani::any

pub fn any<T: Arbitrary>() -> T

This creates an symbolic valid value of type T. You can assign the return value of this function to a variable that you want to make symbolic.

Example:

In the snippet below, we are verifying the behavior of the function fn_under_verification under all possible NonZeroU8 input values, i.e., all possible u8 values except zero.

let inputA = kani::any::<std::num::NonZeroU8>();
fn_under_verification(inputA);

Note: This is a safe construct and can only be used with types that implement the Arbitrary trait. The Arbitrary trait is used to build a symbolic value that represents all possible valid values for type T.