Can't write contracts for functions that return mutable references to input arguments

[carolynzech]

I tried this code:

#[kani::requires(*val != 0)]
unsafe fn foo(val: &mut u8) -> &mut u8 {
    val
}

#[kani::proof]
fn harness() {
    let mut x: u8 = kani::any();
    unsafe { foo(&mut x) };
}

using the following command line invocation:

cargo kani

with Kani version: 0.56

I expected to see this happen: verification success

Instead, this happened:

error: captured variable cannot escape `FnMut` closure body
  --> src/lib.rs:12:5
   |
11 | unsafe fn foo(val: &mut u8) -> &mut u8 {
   |               ---              - inferred to be a `FnMut` closure
   |               |
   |               variable defined here
12 |     val
   |     ^^^
   |     |
   |     returns a reference to a captured variable which escapes the closure body
   |     variable captured here
   |
   = note: `FnMut` closures only have access to their captured variables while they are executing...
   = note: ...therefore, they cannot allow references to captured variables to escape

error: captured variable cannot escape `FnMut` closure body
  --> src/lib.rs:10:1
   |
10 | #[kani::requires(*val != 0)]
   | ^^^^^^^^^^^^^^^^^^---^^^^^^^
   | |                 |
   | |                 variable captured here
   | returns a reference to a captured variable which escapes the closure body
11 | unsafe fn foo(val: &mut u8) -> &mut u8 {
   |               ---              - inferred to be a `FnMut` closure
   |               |
   |               variable defined here
   |
   = note: `FnMut` closures only have access to their captured variables while they are executing...
   = note: ...therefore, they cannot allow references to captured variables to escape
   = note: this error originates in the attribute macro `kani::requires` (in Nightly builds, run with -Z macro-backtrace for more info)

This is a minimal reproducer of a problem encountered trying to write contracts for NonZero::from_mut_unchecked, which has this function signature:

pub unsafe fn from_mut_unchecked(n: &mut T) -> &mut Self