Apply suggestions from code review

Co-authored-by: Carolyn Zech <cmzech@amazon.com>

kani-compiler/src/kani_middle/transform/kani_intrinsics.rs

@@ -404,7 +404,7 @@ impl IntrinsicGeneratorPass {
         let ptr_arg = body.arg_locals().first().expect("Expected a pointer argument");
         let ptr_ty = ptr_arg.ty;
         let TyKind::RigidTy(RigidTy::RawPtr(pointee_ty, _)) = ptr_ty.kind() else {
-            unreachable!("Expected a pointer argument,but got {ptr_ty}")
+            unreachable!("Expected a pointer argument, but got {ptr_ty}")
         };
         let pointee_layout = LayoutOf::new(pointee_ty);
         debug!(?ptr_ty, ?pointee_layout, "checked_size_of");
@@ -530,7 +530,7 @@ impl IntrinsicGeneratorPass {
         let ptr_arg = body.arg_locals().first().expect("Expected a pointer argument");
         let ptr_ty = ptr_arg.ty;
         let TyKind::RigidTy(RigidTy::RawPtr(pointee_ty, _)) = ptr_ty.kind() else {
-            unreachable!("Expected a pointer argument,but got {ptr_ty}")
+            unreachable!("Expected a pointer argument, but got {ptr_ty}")
         };
         let pointee_layout = LayoutOf::new(pointee_ty);
         debug!(?ptr_ty, "align_of_raw");
@@ -572,7 +572,11 @@ impl IntrinsicGeneratorPass {
             );
         } else {
             // Cannot compute size of foreign types. Return None!
-            assert!(pointee_layout.has_foreign_tail());
+            assert!(
+                pointee_layout.has_foreign_tail(),
+                "Expected foreign, but found `{:?}` tail instead.",
+                pointee_layout.unsized_tail()
+            );
             let ret_val = build_none(option_def, option_args);
             new_body.assign_to(
                 Place::from(RETURN_LOCAL),
@@ -605,6 +609,7 @@ impl IntrinsicGeneratorPass {
 }
 
 /// Build an Rvalue `Some(val)`.
+/// Since the variants of `Option` are `Some(val)` and `None`, we know we've found the `Some` variant when we find the first variant with a field.
 fn build_some(option: AdtDef, args: GenericArgs, val_op: Operand) -> Rvalue {
     let var_idx = option
         .variants_iter()
@@ -614,6 +619,7 @@ fn build_some(option: AdtDef, args: GenericArgs, val_op: Operand) -> Rvalue {
 }
 
 /// Build an Rvalue `None`.
+/// Since the variants of `Option` are `Some(val)` and `None`, we know we've found the `None` variant when we find the first variant without fields.
 fn build_none(option: AdtDef, args: GenericArgs) -> Rvalue {
     let var_idx =
         option.variants_iter().find_map(|var| var.fields().is_empty().then_some(var.idx)).unwrap();

library/kani_core/src/mem.rs

@@ -152,7 +152,7 @@ macro_rules! kani_mem {
             cbmc::same_allocation(ptr1, ptr2)
         }
 
-        /// Compute the size of the val pointed to if safe.
+        /// Compute the size of the val pointed to if it is safe to do so.
         ///
         /// Return `None` if an overflow would occur, or if alignment is not power of two.
         /// TODO: Optimize this if T is sized.

library/kani_core/src/models.rs

@@ -33,7 +33,7 @@ macro_rules! generate_models {
                 if align.is_power_of_two() {
                     let size_dyn = metadata.size_of();
                     let (total, sum_overflow) = size_dyn.overflowing_add(head_size);
-                    // Adjust size to be a multiple of alignment, i.e.: (size + (align - 1)) & -align
+                    // Round up size to the nearest multiple of alignment, i.e.: (size + (align - 1)) & -align
                     let (adjust, adjust_overflow) = total.overflowing_add(align.wrapping_sub(1));
                     let adjusted_size = adjust & align.wrapping_neg();
                     if sum_overflow || adjust_overflow || adjusted_size > isize::MAX as _ {
@@ -80,7 +80,7 @@ macro_rules! generate_models {
             ) -> Option<usize> {
                 let (slice_sz, mul_overflow) = elem_size.overflowing_mul(len);
                 let (total, sum_overflow) = slice_sz.overflowing_add(head_size);
-                // Adjust size to be a multiple of alignment, i.e.: (size + (align - 1)) & -align
+                // Round up size to the nearest multiple of alignment, i.e.: (size + (align - 1)) & -align
                 let (adjust, adjust_overflow) = total.overflowing_add(align.wrapping_sub(1));
                 let adjusted_size = adjust & align.wrapping_neg();
                 if mul_overflow