Wrap assert!(is_initialized(...)) into a separate function

library/kani/src/mem.rs

@@ -122,13 +122,7 @@ where
  // not make sense to use it inside assumption context.
  metadata.is_ptr_aligned(thin_ptr, Internal)
  && is_inbounds(&metadata, thin_ptr)
- && {
- crate::assert(
- is_initialized(ptr, 1),
- "Undefined Behavior: Reading from an uninitialized pointer",
- );
- true
- }
+ && assert_is_initialized(ptr)
  && unsafe { has_valid_value(ptr) }
 }
 
@@ -159,13 +153,7 @@ where
  // Need to assert `is_initialized` because non-determinism is used under the hood, so it does
  // not make sense to use it inside assumption context.
  is_inbounds(&metadata, thin_ptr)
- && {
- crate::assert(
- is_initialized(ptr, 1),
- "Undefined Behavior: Reading from an uninitialized pointer",
- );
- true
- }
+ && assert_is_initialized(ptr)
  && unsafe { has_valid_value(ptr) }
 }
 
@@ -316,6 +304,15 @@ pub fn is_initialized<T: ?Sized>(_ptr: *const T, _len: usize) -> bool {
  kani_intrinsic()
 }
 
+/// A helper to to assert `is_initialized` to use it as a part of other predicates.
+fn assert_is_initialized<T: ?Sized>(ptr: *const T) -> bool {
+ crate::assert(
+ is_initialized(ptr, 1),
+ "Undefined Behavior: Reading from an uninitialized pointer",
+ );
+ true
+}
+
 /// Get the object ID of the given pointer.
 #[rustc_diagnostic_item = "KaniPointerObject"]
 #[inline(never)]

library/kani_core/src/mem.rs

@@ -127,13 +127,7 @@ macro_rules! kani_mem {
  // does not make sense to use it inside assumption context.
  metadata.is_ptr_aligned(thin_ptr, Internal)
  && is_inbounds(&metadata, thin_ptr)
- && {
- assert!(
- is_initialized(ptr, 1),
- "Undefined Behavior: Reading from an uninitialized pointer",
- );
- true
- }
+ && assert_is_initialized(ptr)
  && unsafe { has_valid_value(ptr) }
  }
 
@@ -165,13 +159,7 @@ macro_rules! kani_mem {
  // Need to assert `is_initialized` because non-determinism is used under the hood, so it
  // does not make sense to use it inside assumption context.
  is_inbounds(&metadata, thin_ptr)
- && {
- assert!(
- is_initialized(ptr, 1),
- "Undefined Behavior: Reading from an uninitialized pointer",
- );
- true
- }
+ && assert_is_initialized(ptr)
  && unsafe { has_valid_value(ptr) }
  }
 
@@ -322,6 +310,15 @@ macro_rules! kani_mem {
  kani_intrinsic()
  }
 
+ /// A helper to to assert `is_initialized` to use it as a part of other predicates.
+ fn assert_is_initialized<T: ?Sized>(ptr: *const T) -> bool {
+ assert!(
+ is_initialized(ptr, 1),
+ "Undefined Behavior: Reading from an uninitialized pointer",
+ );
+ true
+ }
+
  /// Get the object ID of the given pointer.
  #[rustc_diagnostic_item = "KaniPointerObject"]
  #[inline(never)]