Failed check: memmove.assigns in Memory operations API

[Dhvani-Kapadia]

I ran into a failed check for both copy_to and copy_from API. Can a clause be added to the contract to make it successful? The exact error message is:
Failure without assigns: Check 7: memmove.assigns.2 - Status: FAILURE - Description: "Check that array_replace((const void *)(char *)dest, ...) is allowed by the assigns clause" - Location: <builtin-library-memmove>:34 in function memmove

This is the contract I wrote for copy_to:
`#[kani::requires(count * core::mem::size_of::() <= isize::MAX as usize)]

#[requires(
    ub_checks::can_dereference(self.as_ptr() as *const T, count * core::mem::size_of::<T>()) &&//The pointer is valid for the specified number of elements of type T.
    self.as_ptr() as usize % core::mem::align_of::<T>() == 0 //The pointer is properly aligned for type T
)]

#[requires(
    ub_checks::can_dereference(dest.as_ptr() as *const T, count * core::mem::size_of::<T>())) &&//The pointer is valid for the specified number of elements of type T.
    dest.as_ptr() as usize % core::mem::align_of::<T>() == 0 //The pointer is properly aligned for type T
]

#[ensures(|result: &()| ub_checks::can_dereference(self.as_ptr() as *const T, count * core::mem::size_of::<T>()))]

#[ensures(|result: &()| ub_checks::can_dereference(dest.as_ptr() as *const T, count * core::mem::size_of::<T>()))]` @zhassan-aws , @feliperodri 

[danielhumanmod]

I have the same error for swap(), here is the function contract and proof harness:

    #[inline(always)]
    #[stable(feature = "non_null_convenience", since = "1.80.0")]
    #[rustc_const_unstable(feature = "const_swap", issue = "83163")]
    #[requires(self.as_ptr().align_offset(core::mem::align_of::<T>()) == 0)]
    #[requires(with.as_ptr().align_offset(core::mem::align_of::<T>()) == 0)]
    #[requires(ub_checks::can_dereference(self.as_ptr()))]
    #[requires(ub_checks::can_dereference(with.as_ptr()))]
    pub const unsafe fn swap(self, with: NonNull<T>)
    where
        T: Sized,
    {
        // SAFETY: the caller must uphold the safety contract for `swap`.
        unsafe { ptr::swap(self.as_ptr(), with.as_ptr()) }
    }

    #[kani::proof_for_contract(NonNull::swap)]
    pub fn non_null_check_swap() {
        let mut a: i32 = kani::any();
        let mut b: i32 = kani::any();

        let ptr_a = NonNull::new(&mut a as *mut i32).unwrap();
        let ptr_b = NonNull::new(&mut b as *mut i32).unwrap();

        unsafe {
            let old_a = ptr::read(ptr_a.as_ptr());
            let old_b = ptr::read(ptr_b.as_ptr());
            ptr_a.swap(ptr_b);
            // Verify that the values have been swapped.
            let new_a = ptr::read(ptr_a.as_ptr());
            let new_b = ptr::read(ptr_b.as_ptr());
            kani::assume(old_a == new_b);
            kani::assume(old_b == new_a);
        }
    }

[zhassan-aws]

Hi @Dhvani-Kapadia, @danielhumanmod. Both functions modify the object, so a modifies-clause is needed. See https://model-checking.github.io/kani/crates/doc/kani/contracts/index.html#write-sets for details. You can also look at some examples in https://github.com/model-checking/kani/tree/main/tests/expected/function-contract/modifies.

[danielhumanmod]

Thanks Zyad, it works after adding kani:: modifies, really appreciate for your input!