[Feature Request] Ability to stub out function on primitive types (such as [T]) #2646
Description
Requested feature: I recently ran across a situation where I wanted to stub the binary_search_by_key function on slices because I knew my slice would always have length 1, which would allow me to save on some unrolls. I ran into some problems expressing this stub however, since [T]::binary_search_by_key is not a valid path (even the impl [T] in the standard library seems to be special-cased into the compiler).
Test case:
I'm really not sure how to express this, since [T] cannot really be part of paths, but I guess I'd like
// kani_example.rs
fn stub_len<T>(this: &[T]) -> usize {
0
}
#[kani::proof]
#[kani::stub(std::slice::[T]::len, stub_len)]
fn verify_len() {
assert_eq!(vec![1].as_slice().len(), 0);
}to work. Currently, the output I get from running kani kani_example.rs is
$ kani kani_example.rs
Kani Rust Verifier 0.33.0 (standalone)
warning: unused variable: `this`
--> kani_example.rs:1:16
|
1 | fn stub_len<T>(this: &[T]) -> usize {
| ^^^^ help: if this is intentional, prefix it with an underscore: `_this`
|
= note: `#[warn(unused_variables)]` on by default
warning: function `stub_len` is never used
--> kani_example.rs:1:4
|
1 | fn stub_len<T>(this: &[T]) -> usize {
| ^^^^^^^^
|
= note: `#[warn(dead_code)]` on by default
error: attribute `kani::stub` takes two path arguments; found 0
--> kani_example.rs:6:1
|
6 | #[kani::stub(std::slice::[T]::len, stub_len)]
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
|
= note: this error originates in the attribute macro `kani::stub` (in Nightly builds, run with -Z macro-backtrace for more info)