From 7cfe27c589185eb94f7c37230551503652b2c61d Mon Sep 17 00:00:00 2001 From: zjp Date: Thu, 21 Aug 2025 10:24:25 +0000 Subject: [PATCH] fix upstream monomorphizations errors by inlining kani_contract_mode MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit error: `compiler_builtins` cannot call functions through upstream monomorphizations; encountered invalid call from `core::ops::index_range::IndexRange::next_unchecked` to `core::ops::index_range::IndexRange::next_unchecked::kani_contract_mode` --> /home/gh-zjp-CN/distributed-verification/verify-rust-std/library/core/src/ops/index_range.rs:63:5 | 63 | #[cfg_attr(kani, kani::modifies(self))] // 👈 annotated on core::ops::index_range::IndexRange::next_unchecked | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ in this attribute macro expansion --- library/kani_macros/src/sysroot/contracts/bootstrap.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/kani_macros/src/sysroot/contracts/bootstrap.rs b/library/kani_macros/src/sysroot/contracts/bootstrap.rs index ed8bde7f8974..d8f2eae87435 100644 --- a/library/kani_macros/src/sysroot/contracts/bootstrap.rs +++ b/library/kani_macros/src/sysroot/contracts/bootstrap.rs @@ -71,7 +71,7 @@ impl<'a> ContractConditionsHandler<'a> { } // Dummy function that we replace to pick the contract mode. // By default, return ORIGINAL - #[inline(never)] + #[inline] #[kanitool::fn_marker = "kani_contract_mode"] const fn kani_contract_mode() -> kani::internal::Mode { kani::internal::ORIGINAL