Kani contract cannot be applied to functions with rustc_diagnostic_item #3251
Description
I tried this code (on the core crate):
#[inline]
#[kani_core::requires(ub_checks::can_dereference(src))]
#[stable(feature = "volatile", since = "1.9.0")]
#[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
#[rustc_diagnostic_item = "ptr_read_volatile"]
pub unsafe fn read_volatile<T>(src: *const T) -> T {
// ..
}using the following command line invocation:
kani verify-std ./library/ -Z unstable-options --target-dir target/verify-std
with Kani version:
I expected to see this happen: 0.52.0
Instead, this happened: Kani failed to compile the code:
error: duplicate diagnostic item in crate `core`: `ptr_read_volatile`.
--> library/core/src/ptr/mod.rs:1693:1
|
1693 | pub unsafe fn read_volatile<T>(src: *const T) -> T {
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
|
note: the diagnostic item is first defined here
--> library/core/src/ptr/mod.rs:1689:1
|
1689 | #[kani_core::requires(ub_checks::can_dereference(src))]
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
= note: this error originates in the attribute macro `kani_core::requires` (in Nightly builds, run with -Z macro-backtrace for more info)