filter out zsts for cmbc assigns for contracts

kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs

@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-use crate::codegen_cprover_gotoc::GotocCtx;
+use crate::codegen_cprover_gotoc::{codegen::ty_stable::pointee_type_stable, GotocCtx};
 use crate::kani_middle::attributes::KaniAttributes;
 use cbmc::goto_program::FunctionContract;
 use cbmc::goto_program::{Expr, Lambda, Location, Type};
@@ -160,11 +160,17 @@ impl<'tcx> GotocCtx<'tcx> {
         let TyKind::RigidTy(RigidTy::Tuple(modifies_tys)) = modifies_ty.kind() else {
             unreachable!("found {:?}", modifies_ty.kind())
         };
+
+        for ty in &modifies_tys {
+            assert!(ty.kind().is_any_ptr(), "Expected pointer, but found {}", ty);
+        }
+
         let assigns: Vec<_> = modifies_tys
             .into_iter()
+            // do not attempt to dereference (and assign) a ZST
+            .filter(|ty| !self.is_zst_stable(pointee_type_stable(*ty).unwrap()))
             .enumerate()
             .map(|(idx, ty)| {
-                assert!(ty.kind().is_any_ptr(), "Expected pointer, but found {}", ty);
                 let ptr = modifies_args.clone().member(idx.to_string(), &self.symbol_table);
                 if self.is_fat_pointer_stable(ty) {
                     let unref = match ty.kind() {

tests/expected/function-contract/modifies/zst_pass.rs

@@ -2,8 +2,6 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: -Zfunction-contracts
 
-// #[kani::requires(assert_valid_ptr(dst) && has_valid_value(dst))]
-#[kani::requires(true)]
 #[kani::modifies(dst)]
 pub unsafe fn replace<T>(dst: *mut T, src: T) -> T {
     std::ptr::replace(dst, src)
@@ -21,4 +19,4 @@ fn check_replace_impl<T: kani::Arbitrary + Eq + Clone>() {
     let ret = unsafe { replace(&mut dst, src.clone()) };
     assert_eq!(ret, orig);
     assert_eq!(dst, src);
-}
+}