Minor changes

kani-compiler/src/kani_middle/transform/check_uninit/mod.rs

@@ -425,7 +425,8 @@ impl<'a, 'tcx> UninitInstrumenter<'a, 'tcx> {
             }
             PointeeLayout::Union { field_layouts } => {
                 // Writing union data, which could be either creating a union from scratch or
-                // performing some pointer operations with it.
+                // performing some pointer operations with it. If we are creating a union from
+                // scratch, an operation will contain a union field.
 
                 // TODO: If we don't have a union field, we are either creating a pointer to a union
                 // or assigning to one. In the former case, it is safe to return from this function,

kani-compiler/src/kani_middle/transform/check_uninit/relevant_instruction.rs

@@ -7,7 +7,7 @@
 use crate::kani_middle::transform::body::{InsertPosition, MutableBody, SourceInstruction};
 use stable_mir::{
     mir::{FieldIdx, Mutability, Operand, Place, Rvalue, Statement, StatementKind},
-    ty::Ty,
+    ty::{RigidTy, Ty},
 };
 use strum_macros::AsRefStr;
 
@@ -152,9 +152,19 @@ impl MemoryInitOp {
             MemoryInitOp::Unsupported { .. } | MemoryInitOp::TriviallyUnsafe { .. } => {
                 unreachable!("operands do not exist for this operation")
             }
-            MemoryInitOp::Copy { from, .. } => {
+            MemoryInitOp::Copy { from, to, .. } => {
                 // It does not matter which operand to return for layout generation, since both of
-                // them have the same pointee type.
+                // them have the same pointee type, so we assert that.
+                let from_kind = from.ty(body.locals()).unwrap().kind();
+                let to_kind = to.ty(body.locals()).unwrap().kind();
+
+                let RigidTy::RawPtr(from_pointee_ty, _) = from_kind.rigid().unwrap().clone() else {
+                    unreachable!()
+                };
+                let RigidTy::RawPtr(to_pointee_ty, _) = to_kind.rigid().unwrap().clone() else {
+                    unreachable!()
+                };
+                assert!(from_pointee_ty == to_pointee_ty);
                 from.ty(body.locals()).unwrap()
             }
             MemoryInitOp::AssignUnion { lvalue, .. } => {