Function kani::any_where

pub fn any_where<T: Arbitrary, F: FnOnce(&T) -> bool>(f: F) -> T

This creates a symbolic valid value of type T. The value is constrained to be a value accepted by the predicate passed to the filter. 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 u8 input values between 0 and 12.

let inputA: u8 = kani::any_where(|x| *x < 12);
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.