`kani::modifies` causes an error that compiler_builtins cannot call functions through upstream monomorphizations

[zjp-CN]

When I run dv on current verify-rust-std@ca49535, I got a compilation error as follows.
When I comment out kani::modifies just in this place, all crates compile fine. (NOTE there are some other modifies clauses around, and they don't bring any error except this annotation.)

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))]
    |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ in this attribute macro expansion
    |
   ::: /home/gh-zjp-CN/distributed-verification/kani/library/kani_macros/src/lib.rs:427:1
    |
427 | pub fn modifies(attr: TokenStream, item: TokenStream) -> TokenStream {
    | -------------------------------------------------------------------- in this expansion of `#[kani::modifies]`

Mentioned src localtions:

• verify-rust-std/library/core/src/ops/index_range.rs:63:5
• kani/library/kani_macros/src/lib.rs:427:1

Also commented in

• error: compiler_builtins cannot call functions through upstream monomorphizations os-checker/distributed-verification#111
• -Zbuild-std shouldn't explode on compiler-builtins fragility rust-lang/rust#137222 (comment)

[tautschnig]

Could you please check if this gets back to a working state when changing #[cfg_attr(kani, kani::modifies(self))] to #[cfg_attr(kani, kani::modifies(self.as_ptr()))]? (I believe this is what we need to do everywhere.)

[zjp-CN]

&mut has no .as_ptr() method:

error[E0599]: no method named `as_ptr` found for mutable reference `&mut ops::index_range::IndexRange` in the current scope
  --> /home/gh-zjp-CN/distributed-verification/verify-rust-std/library/core/src/ops/index_range.rs:63:42
   |
63 |     #[cfg_attr(kani, kani::modifies(self.as_ptr()))]
   |                                          ^^^^^^ method not found in `&mut ops::index_range::IndexRange`

The fix to make things work I tried is:

when I replace kani_contract_mode's #[inline(never)] with #[inline], verify-rust-std compiles!
(Removing #[inline(never)] still errs.)

Is there a reason to mark them #[inline(never)]?

[zjp-CN]

I've opened model-checking/kani#4312 to fix this issue. For more contexts or explanations, refer to rust-lang#137222 (comment) and following comments.