Let's say you have a crate crate_a that defines a copy_val function that is annotated with contracts:

///----- Crate with contract
#[requires(kani::mem::can_dereference(ptr))]
pub unsafe fn copy_val<T: Copy>(ptr: *const T) -> T {
}

Now we have a crate crate_b that uses crate_a that we want to verify using Kani:

pub fn safe_copy<T: Copy>(x: &T) -> T {
    unsafe { copy_val(x) }
}

using the following command line invocation:

cargo kani --only-codegen

with Kani version: 0.56.0

I expected to see this happen: Compilation should succeed.

Instead, this happened: Kani will fail to compile crate_a due to missing trait bounds.