Fix assert order

model-checking · Jul 3, 2024 · ed11c8e · ed11c8e
1 parent bb2a02b
commit ed11c8e
Show file tree

Hide file tree

Showing 2 changed files with 32 additions and 6 deletions.
diff --git a/library/kani/src/mem.rs b/library/kani/src/mem.rs
@@ -120,9 +120,15 @@ where
     let (thin_ptr, metadata) = ptr.to_raw_parts();
     // 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.
-    assert!(is_initialized(ptr, 1));
     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
+        }
         && unsafe { has_valid_value(ptr) }
 }
 
@@ -152,8 +158,15 @@ where
     let (thin_ptr, metadata) = ptr.to_raw_parts();
     // 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.
-    assert!(is_initialized(ptr, 1));
-    is_inbounds(&metadata, thin_ptr) && unsafe { has_valid_value(ptr) }
+    is_inbounds(&metadata, thin_ptr)
+        && {
+            crate::assert(
+                is_initialized(ptr, 1),
+                "Undefined Behavior: Reading from an uninitialized pointer",
+            );
+            true
+        }
+        && unsafe { has_valid_value(ptr) }
 }
 
 /// Checks that `data_ptr` points to an allocation that can hold data of size calculated from `T`.

diff --git a/library/kani_core/src/mem.rs b/library/kani_core/src/mem.rs
@@ -125,9 +125,15 @@ macro_rules! kani_mem {
             let (thin_ptr, metadata) = ptr.to_raw_parts();
             // 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.
-            assert!(is_initialized(ptr, 1));
             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
+                }
                 && unsafe { has_valid_value(ptr) }
         }
 
@@ -158,8 +164,15 @@ macro_rules! kani_mem {
             let (thin_ptr, metadata) = ptr.to_raw_parts();
             // 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.
-            assert!(is_initialized(ptr, 1));
-            is_inbounds(&metadata, thin_ptr) && unsafe { has_valid_value(ptr) }
+            is_inbounds(&metadata, thin_ptr)
+                && {
+                    crate::assert(
+                        is_initialized(ptr, 1),
+                        "Undefined Behavior: Reading from an uninitialized pointer",
+                    );
+                    true
+                }
+                && unsafe { has_valid_value(ptr) }
         }
 
         /// Checks that `data_ptr` points to an allocation that can hold data of size calculated from `T`.