Break down large visitor functions in instrumentation visitors

kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/instrumentation_visitor.rs

@@ -154,13 +154,7 @@ impl<'a, 'tcx> InstrumentationVisitor<'a, 'tcx> {
                 self.check_operand(cond);
             }
             TerminatorKind::Drop { place, .. } => {
-                // According to the documentation, "After drop elaboration: Drop terminators are a
-                // complete nop for types that have no drop glue. For other types, Drop terminators
-                // behave exactly like a call to core::mem::drop_in_place with a pointer to the
-                // given place." Since we check arguments when instrumenting function calls, perhaps
-                // we need to check that one, too. For more info, see:
-                // https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/enum.TerminatorKind.html#variant.Drop
-                self.check_place(place, PlaceOperation::Read);
+                self.check_place(place, PlaceOperation::Deinit);
             }
             TerminatorKind::Call { func, args, destination, target: _, unwind: _ } => {
                 self.check_operand(func);
@@ -221,7 +215,8 @@ impl<'a, 'tcx> InstrumentationVisitor<'a, 'tcx> {
             }
             Operand::Constant(_) => {
                 // Those should be safe to skip, as they are either constants or statics. In the
-                // latter case, we handle them in regular uninit visior
+                // latter case, we handle them in regular uninit visitor, as accessing statics
+                // requires dereferencing a raw pointer.
             }
         }
     }
@@ -237,23 +232,23 @@ impl<'a, 'tcx> InstrumentationVisitor<'a, 'tcx> {
         {
             match place_operation {
                 PlaceOperation::Write => {
-                    // If we are mutating the place, initialize it.
+                    // Write to the place initializes it.
                     self.push_target(MemoryInitOp::SetRef {
                         operand: Operand::Copy(place.clone()),
                         value: true,
                         position: InsertPosition::After,
                     })
                 }
                 PlaceOperation::Deinit => {
-                    // If we are mutating the place, initialize it.
+                    // Explicitly deinitialie the place.
                     self.push_target(MemoryInitOp::SetRef {
                         operand: Operand::Copy(place.clone()),
                         value: false,
                         position: InsertPosition::After,
                     })
                 }
                 PlaceOperation::Read => {
-                    // Otherwise, check its initialization.
+                    // When reading from a place, check its initialization.
                     self.push_target(MemoryInitOp::CheckRef {
                         operand: Operand::Copy(place.clone()),
                     });