From 756d93871080bea886eee22604ba1a87064e1b2e Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 28 Jan 2025 13:09:24 +0000
Subject: [PATCH 01/10] Adjust PropertyClass of assertions to identify UB

Anything listed as undefined behavior (UB) at
https://doc.rust-lang.org/reference/behavior-considered-undefined.html
must also be considered UB by Kani and should not pass under
`should_fail`. In preparation of this PR, all occurrences of
`PropertyClass` in the code base were audited and, where necessary,
adjusted.

Also, all uses of `kani::assert` were audited to confirm or adjust them.
This resulted in first-time use of the `UnsupportedCheck` hook, which
implied fixes to its implementation.

Resolves: #3571
---
 .../codegen/statement.rs                      | 18 +++++++----
 .../codegen_cprover_gotoc/overrides/hooks.rs  | 31 ++++++++++---------
 library/kani_core/src/mem.rs                  | 19 ++++++------
 .../adt_with_metadata.rs                      |  1 -
 .../fat_ptr_validity.rs                       |  2 --
 tests/expected/issue-3571/issue_3571.expected |  2 ++
 tests/expected/issue-3571/issue_3571.rs       | 13 ++++++++
 .../thin_ptr_validity.rs                      |  2 --
 .../uninit/multiple-instrumentations.expected |  8 ++---
 9 files changed, 57 insertions(+), 39 deletions(-)
 rename tests/{kani/MemPredicates => expected}/adt_with_metadata.rs (98%)
 rename tests/{kani/MemPredicates => expected}/fat_ptr_validity.rs (97%)
 create mode 100644 tests/expected/issue-3571/issue_3571.expected
 create mode 100644 tests/expected/issue-3571/issue_3571.rs
 rename tests/{kani/MemPredicates => expected}/thin_ptr_validity.rs (96%)

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
index 90635a71f2e8..ed7030f5087d 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
@@ -251,19 +251,25 @@ impl GotocCtx<'_> {
                     if *expected { r } else { Expr::not(r) }
                 };
 
-                let msg = if let AssertMessage::BoundsCheck { .. } = msg {
+                let (msg, property_class) = if let AssertMessage::BoundsCheck { .. } = msg {
                     // For bounds check the following panic message is generated at runtime:
                     // "index out of bounds: the length is {len} but the index is {index}",
                     // but CBMC only accepts static messages so we don't add values to the message.
-                    "index out of bounds: the length is less than or equal to the given index"
+                    (
+                        "index out of bounds: the length is less than or equal to the given index",
+                        PropertyClass::Assertion,
+                    )
                 } else if let AssertMessage::MisalignedPointerDereference { .. } = msg {
                     // Misaligned pointer dereference check messages is also a runtime messages.
                     // Generate a generic one here.
-                    "misaligned pointer dereference: address must be a multiple of its type's \
-                    alignment"
+                    (
+                        "misaligned pointer dereference: address must be a multiple of its type's \
+                    alignment",
+                        PropertyClass::SafetyCheck,
+                    )
                 } else {
                     // For all other assert kind we can get the static message.
-                    msg.description().unwrap()
+                    (msg.description().unwrap(), PropertyClass::Assertion)
                 };
 
                 let (msg_str, reach_stmt) =
@@ -274,7 +280,7 @@ impl GotocCtx<'_> {
                         reach_stmt,
                         self.codegen_assert_assume(
                             cond.cast_to(Type::bool()),
-                            PropertyClass::Assertion,
+                            property_class,
                             &msg_str,
                             loc,
                         ),
diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs
index 73c887b3eeaf..c346b60023aa 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs
@@ -160,24 +160,25 @@ impl GotocHook for UnsupportedCheck {
         target: Option<BasicBlockIdx>,
         span: Span,
     ) -> Stmt {
-        assert_eq!(fargs.len(), 2);
+        assert_eq!(fargs.len(), 1);
         let msg = fargs.pop().unwrap();
-        let cond = fargs.pop().unwrap().cast_to(Type::bool());
         let msg = gcx.extract_const_message(&msg).unwrap();
-        let target = target.unwrap();
         let caller_loc = gcx.codegen_caller_span_stable(span);
-        Stmt::block(
-            vec![
-                gcx.codegen_assert_assume(
-                    cond,
-                    PropertyClass::UnsupportedConstruct,
-                    &msg,
-                    caller_loc,
-                ),
-                Stmt::goto(bb_label(target), caller_loc),
-            ],
-            caller_loc,
-        )
+        if let Some(target) = target {
+            Stmt::block(
+                vec![
+                    gcx.codegen_assert_assume_false(
+                        PropertyClass::UnsupportedConstruct,
+                        &msg,
+                        caller_loc,
+                    ),
+                    Stmt::goto(bb_label(target), caller_loc),
+                ],
+                caller_loc,
+            )
+        } else {
+            gcx.codegen_assert_assume_false(PropertyClass::UnsupportedConstruct, &msg, caller_loc)
+        }
     }
 }
 
diff --git a/library/kani_core/src/mem.rs b/library/kani_core/src/mem.rs
index c09d67ca51ff..fb1f1463df6f 100644
--- a/library/kani_core/src/mem.rs
+++ b/library/kani_core/src/mem.rs
@@ -210,10 +210,11 @@ macro_rules! kani_mem {
                 // stubbed.
                 // We first assert that the data_ptr
                 let data_ptr = ptr as *const ();
-                super::assert(
-                    unsafe { is_allocated(data_ptr, 0) },
-                    "Kani does not support reasoning about pointer to unallocated memory",
-                );
+                if !unsafe { is_allocated(data_ptr, 0) } {
+                    crate::kani::unsupported(
+                        "Kani does not support reasoning about pointer to unallocated memory",
+                    );
+                }
                 unsafe { is_allocated(data_ptr, sz) }
             }
         }
@@ -280,11 +281,11 @@ macro_rules! kani_mem {
             pub fn same_allocation(addr1: *const (), addr2: *const ()) -> bool {
                 let obj1 = crate::kani::mem::pointer_object(addr1);
                 (obj1 == crate::kani::mem::pointer_object(addr2)) && {
-                    // TODO(3571): This should be a unsupported check
-                    crate::kani::assert(
-                        unsafe { is_allocated(addr1, 0) || is_allocated(addr2, 0) },
-                        "Kani does not support reasoning about pointer to unallocated memory",
-                    );
+                    if !unsafe { is_allocated(addr1, 0) || is_allocated(addr2, 0) } {
+                        crate::kani::unsupported(
+                            "Kani does not support reasoning about pointer to unallocated memory",
+                        );
+                    }
                     unsafe { is_allocated(addr1, 0) && is_allocated(addr2, 0) }
                 }
             }
diff --git a/tests/kani/MemPredicates/adt_with_metadata.rs b/tests/expected/adt_with_metadata.rs
similarity index 98%
rename from tests/kani/MemPredicates/adt_with_metadata.rs
rename to tests/expected/adt_with_metadata.rs
index aa536b26279f..9ec0a3787964 100644
--- a/tests/kani/MemPredicates/adt_with_metadata.rs
+++ b/tests/expected/adt_with_metadata.rs
@@ -42,7 +42,6 @@ mod invalid_access {
     use super::*;
     use std::ptr;
     #[kani::proof]
-    #[kani::should_panic]
     pub fn check_invalid_dyn_ptr() {
         unsafe fn new_dead_ptr<T>(val: T) -> *const T {
             let local = val;
diff --git a/tests/kani/MemPredicates/fat_ptr_validity.rs b/tests/expected/fat_ptr_validity.rs
similarity index 97%
rename from tests/kani/MemPredicates/fat_ptr_validity.rs
rename to tests/expected/fat_ptr_validity.rs
index c4f037f3a646..f39392b62c5c 100644
--- a/tests/kani/MemPredicates/fat_ptr_validity.rs
+++ b/tests/expected/fat_ptr_validity.rs
@@ -38,14 +38,12 @@ mod valid_access {
 mod invalid_access {
     use super::*;
     #[kani::proof]
-    #[kani::should_panic]
     pub fn check_invalid_dyn_ptr() {
         let raw_ptr: *const dyn PartialEq<u8> = unsafe { new_dead_ptr::<u8>(0) };
         assert!(can_dereference(raw_ptr));
     }
 
     #[kani::proof]
-    #[kani::should_panic]
     pub fn check_invalid_slice_ptr() {
         let raw_ptr: *const [char] = unsafe { new_dead_ptr::<[char; 2]>(['a', 'b']) };
         assert!(can_dereference(raw_ptr));
diff --git a/tests/expected/issue-3571/issue_3571.expected b/tests/expected/issue-3571/issue_3571.expected
new file mode 100644
index 000000000000..84191346398c
--- /dev/null
+++ b/tests/expected/issue-3571/issue_3571.expected
@@ -0,0 +1,2 @@
+VERIFICATION:- FAILED (encountered failures other than panics, which were unexpected)
+Complete - 0 successfully verified harnesses, 2 failures, 2 total.
diff --git a/tests/expected/issue-3571/issue_3571.rs b/tests/expected/issue-3571/issue_3571.rs
new file mode 100644
index 000000000000..5fc1871f0415
--- /dev/null
+++ b/tests/expected/issue-3571/issue_3571.rs
@@ -0,0 +1,13 @@
+#[kani::proof]
+#[kani::should_panic]
+pub fn rust_ub_fails() {
+    let ptr = 0 as *const u32;
+    let _invalid_ref = unsafe { &*ptr };
+}
+
+#[kani::proof]
+#[kani::should_panic]
+pub fn rust_ub_should_fail() {
+    let ptr = 10 as *const u32;
+    let _invalid_read = unsafe { *ptr };
+}
diff --git a/tests/kani/MemPredicates/thin_ptr_validity.rs b/tests/expected/thin_ptr_validity.rs
similarity index 96%
rename from tests/kani/MemPredicates/thin_ptr_validity.rs
rename to tests/expected/thin_ptr_validity.rs
index 553c5beab9f8..519a07297192 100644
--- a/tests/kani/MemPredicates/thin_ptr_validity.rs
+++ b/tests/expected/thin_ptr_validity.rs
@@ -32,14 +32,12 @@ mod valid_access {
 mod invalid_access {
     use super::*;
     #[kani::proof]
-    #[kani::should_panic]
     pub fn check_invalid_ptr() {
         let raw_ptr = unsafe { new_dead_ptr::<u8>(0) };
         assert!(!can_dereference(raw_ptr));
     }
 
     #[kani::proof]
-    #[kani::should_panic]
     pub fn check_invalid_array() {
         let raw_ptr = unsafe { new_dead_ptr::<[char; 2]>(['a', 'b']) };
         assert!(can_dereference(raw_ptr));
diff --git a/tests/expected/uninit/multiple-instrumentations.expected b/tests/expected/uninit/multiple-instrumentations.expected
index 153024dc692b..413314d8d72e 100644
--- a/tests/expected/uninit/multiple-instrumentations.expected
+++ b/tests/expected/uninit/multiple-instrumentations.expected
@@ -1,16 +1,16 @@
-multiple_instrumentations_different_vars.assertion.3\
+multiple_instrumentations_different_vars.assertion.1\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"
 
-multiple_instrumentations_different_vars.assertion.4\
+multiple_instrumentations_different_vars.assertion.2\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u64`"
 
-multiple_instrumentations.assertion.2\
+multiple_instrumentations.assertion.1\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"
 
-multiple_instrumentations.assertion.3\
+multiple_instrumentations.assertion.2\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"
 

From 136dd83f59e79de63a39c81d9f8a2460240f729a Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 28 Jan 2025 14:53:44 +0000
Subject: [PATCH 02/10] Add copyright

---
 tests/expected/issue-3571/issue_3571.rs | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/tests/expected/issue-3571/issue_3571.rs b/tests/expected/issue-3571/issue_3571.rs
index 5fc1871f0415..c4d55f39b4e4 100644
--- a/tests/expected/issue-3571/issue_3571.rs
+++ b/tests/expected/issue-3571/issue_3571.rs
@@ -1,3 +1,6 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
 #[kani::proof]
 #[kani::should_panic]
 pub fn rust_ub_fails() {

From 0dec9b3865e473e7360819be68010d70d2476d76 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 28 Jan 2025 15:53:43 +0000
Subject: [PATCH 03/10] Fix missing files

---
 tests/expected/MemPredicates/adt_with_metadata.expected | 4 ++++
 tests/expected/{ => MemPredicates}/adt_with_metadata.rs | 0
 tests/expected/MemPredicates/fat_ptr_validity.expected  | 5 +++++
 tests/expected/{ => MemPredicates}/fat_ptr_validity.rs  | 0
 tests/expected/MemPredicates/thin_ptr_validity.expected | 5 +++++
 tests/expected/{ => MemPredicates}/thin_ptr_validity.rs | 0
 6 files changed, 14 insertions(+)
 create mode 100644 tests/expected/MemPredicates/adt_with_metadata.expected
 rename tests/expected/{ => MemPredicates}/adt_with_metadata.rs (100%)
 create mode 100644 tests/expected/MemPredicates/fat_ptr_validity.expected
 rename tests/expected/{ => MemPredicates}/fat_ptr_validity.rs (100%)
 create mode 100644 tests/expected/MemPredicates/thin_ptr_validity.expected
 rename tests/expected/{ => MemPredicates}/thin_ptr_validity.rs (100%)

diff --git a/tests/expected/MemPredicates/adt_with_metadata.expected b/tests/expected/MemPredicates/adt_with_metadata.expected
new file mode 100644
index 000000000000..b3d971a40e61
--- /dev/null
+++ b/tests/expected/MemPredicates/adt_with_metadata.expected
@@ -0,0 +1,4 @@
+Failed Checks: Kani does not support reasoning about pointer to unallocated memory
+
+Verification failed for - invalid_access::check_invalid_dyn_ptr
+Complete - 3 successfully verified harnesses, 1 failures, 4 total.
diff --git a/tests/expected/adt_with_metadata.rs b/tests/expected/MemPredicates/adt_with_metadata.rs
similarity index 100%
rename from tests/expected/adt_with_metadata.rs
rename to tests/expected/MemPredicates/adt_with_metadata.rs
diff --git a/tests/expected/MemPredicates/fat_ptr_validity.expected b/tests/expected/MemPredicates/fat_ptr_validity.expected
new file mode 100644
index 000000000000..b57ca4986e60
--- /dev/null
+++ b/tests/expected/MemPredicates/fat_ptr_validity.expected
@@ -0,0 +1,5 @@
+Failed Checks: Kani does not support reasoning about pointer to unallocated memory
+
+Verification failed for - invalid_access::check_invalid_slice_ptr
+Verification failed for - invalid_access::check_invalid_dyn_ptr
+Complete - 4 successfully verified harnesses, 2 failures, 6 total.
diff --git a/tests/expected/fat_ptr_validity.rs b/tests/expected/MemPredicates/fat_ptr_validity.rs
similarity index 100%
rename from tests/expected/fat_ptr_validity.rs
rename to tests/expected/MemPredicates/fat_ptr_validity.rs
diff --git a/tests/expected/MemPredicates/thin_ptr_validity.expected b/tests/expected/MemPredicates/thin_ptr_validity.expected
new file mode 100644
index 000000000000..54245a84a491
--- /dev/null
+++ b/tests/expected/MemPredicates/thin_ptr_validity.expected
@@ -0,0 +1,5 @@
+Failed Checks: Kani does not support reasoning about pointer to unallocated memory
+
+Verification failed for - invalid_access::check_invalid_array
+Verification failed for - invalid_access::check_invalid_ptr
+Complete - 3 successfully verified harnesses, 2 failures, 5 total.
diff --git a/tests/expected/thin_ptr_validity.rs b/tests/expected/MemPredicates/thin_ptr_validity.rs
similarity index 100%
rename from tests/expected/thin_ptr_validity.rs
rename to tests/expected/MemPredicates/thin_ptr_validity.rs

From 4c7f6c52a637bb048a425fb576b75fa91d56b5b1 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 12 Feb 2025 18:42:55 +0000
Subject: [PATCH 04/10] Rewire MIR-level checks to safety or "unsupported"
 checks

---
 .../codegen_cprover_gotoc/overrides/hooks.rs  | 32 +++++++++
 .../src/kani_middle/kani_functions.rs         |  2 +
 .../src/kani_middle/transform/body.rs         | 69 +++++++++++--------
 .../transform/check_uninit/delayed_ub/mod.rs  | 18 +++--
 .../kani_middle/transform/check_uninit/mod.rs | 46 ++++++++-----
 .../transform/check_uninit/ptr_uninit/mod.rs  |  6 +-
 .../src/kani_middle/transform/check_values.rs | 34 ++++-----
 .../kani_middle/transform/kani_intrinsics.rs  | 50 +++-----------
 .../src/kani_middle/transform/mod.rs          | 27 ++++++--
 library/kani_core/src/lib.rs                  | 12 ++++
 ...s-padding-enum-diverging-variants.expected |  5 ++
 .../access-padding-enum-diverging-variants.rs |  1 -
 ...ss-padding-enum-multiple-variants.expected |  9 +++
 .../access-padding-enum-multiple-variants.rs  |  2 -
 .../access-padding-enum-single-field.expected |  6 ++
 .../access-padding-enum-single-field.rs       |  1 -
 ...ccess-padding-enum-single-variant.expected |  5 ++
 .../access-padding-enum-single-variant.rs     |  1 -
 ...xpected => access-padding-uninit.expected} |  0
 .../valid-value-checks/constants.expected     | 13 ++++
 .../valid-value-checks}/constants.rs          |  3 -
 .../valid-value-checks/custom_niche.expected  | 37 ++++++++++
 .../valid-value-checks}/custom_niche.rs       |  9 ---
 .../valid-value-checks/maybe_uninit.expected  |  5 ++
 .../valid-value-checks}/maybe_uninit.rs       |  1 -
 .../valid-value-checks/non_null.expected      |  9 +++
 .../valid-value-checks}/non_null.rs           |  2 -
 .../valid-value-checks/write_bytes.expected   |  5 ++
 .../valid-value-checks}/write_bytes.rs        |  1 -
 .../valid-value-checks/write_invalid.expected | 13 ++++
 .../valid-value-checks}/write_invalid.rs      |  3 -
 31 files changed, 290 insertions(+), 137 deletions(-)
 create mode 100644 tests/expected/uninit/access-padding-uninit/access-padding-enum-diverging-variants.expected
 rename tests/{kani/Uninit => expected/uninit/access-padding-uninit}/access-padding-enum-diverging-variants.rs (97%)
 create mode 100644 tests/expected/uninit/access-padding-uninit/access-padding-enum-multiple-variants.expected
 rename tests/{kani/Uninit => expected/uninit/access-padding-uninit}/access-padding-enum-multiple-variants.rs (96%)
 create mode 100644 tests/expected/uninit/access-padding-uninit/access-padding-enum-single-field.expected
 rename tests/{kani/Uninit => expected/uninit/access-padding-uninit}/access-padding-enum-single-field.rs (97%)
 create mode 100644 tests/expected/uninit/access-padding-uninit/access-padding-enum-single-variant.expected
 rename tests/{kani/Uninit => expected/uninit/access-padding-uninit}/access-padding-enum-single-variant.rs (97%)
 rename tests/expected/uninit/access-padding-uninit/{expected => access-padding-uninit.expected} (100%)
 create mode 100644 tests/expected/valid-value-checks/constants.expected
 rename tests/{kani/ValidValues => expected/valid-value-checks}/constants.rs (93%)
 create mode 100644 tests/expected/valid-value-checks/custom_niche.expected
 rename tests/{kani/ValidValues => expected/valid-value-checks}/custom_niche.rs (94%)
 create mode 100644 tests/expected/valid-value-checks/maybe_uninit.expected
 rename tests/{kani/ValidValues => expected/valid-value-checks}/maybe_uninit.rs (96%)
 create mode 100644 tests/expected/valid-value-checks/non_null.expected
 rename tests/{kani/ValidValues => expected/valid-value-checks}/non_null.rs (94%)
 create mode 100644 tests/expected/valid-value-checks/write_bytes.expected
 rename tests/{kani/ValidValues => expected/valid-value-checks}/write_bytes.rs (96%)
 create mode 100644 tests/expected/valid-value-checks/write_invalid.expected
 rename tests/{kani/ValidValues => expected/valid-value-checks}/write_invalid.rs (94%)

diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs
index c346b60023aa..e54a1fc4dd9e 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs
@@ -213,6 +213,37 @@ impl GotocHook for SafetyCheck {
     }
 }
 
+struct SafetyCheckNoAssume;
+impl GotocHook for SafetyCheckNoAssume {
+    fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool {
+        unreachable!("{UNEXPECTED_CALL}")
+    }
+
+    fn handle(
+        &self,
+        gcx: &mut GotocCtx,
+        _instance: Instance,
+        mut fargs: Vec<Expr>,
+        _assign_to: &Place,
+        target: Option<BasicBlockIdx>,
+        span: Span,
+    ) -> Stmt {
+        assert_eq!(fargs.len(), 2);
+        let msg = fargs.pop().unwrap();
+        let cond = fargs.pop().unwrap().cast_to(Type::bool());
+        let msg = gcx.extract_const_message(&msg).unwrap();
+        let target = target.unwrap();
+        let caller_loc = gcx.codegen_caller_span_stable(span);
+        Stmt::block(
+            vec![
+                gcx.codegen_assert(cond, PropertyClass::SafetyCheck, &msg, caller_loc),
+                Stmt::goto(bb_label(target), caller_loc),
+            ],
+            caller_loc,
+        )
+    }
+}
+
 // TODO: Remove this and replace occurrences with `SanityCheck`.
 struct Check;
 impl GotocHook for Check {
@@ -739,6 +770,7 @@ pub fn fn_hooks() -> GotocHooks {
         (KaniHook::Cover, Rc::new(Cover)),
         (KaniHook::AnyRaw, Rc::new(Nondet)),
         (KaniHook::SafetyCheck, Rc::new(SafetyCheck)),
+        (KaniHook::SafetyCheckNoAssume, Rc::new(SafetyCheckNoAssume)),
         (KaniHook::IsAllocated, Rc::new(IsAllocated)),
         (KaniHook::PointerObject, Rc::new(PointerObject)),
         (KaniHook::PointerOffset, Rc::new(PointerOffset)),
diff --git a/kani-compiler/src/kani_middle/kani_functions.rs b/kani-compiler/src/kani_middle/kani_functions.rs
index 3182ced8fa61..01d237bf0773 100644
--- a/kani-compiler/src/kani_middle/kani_functions.rs
+++ b/kani-compiler/src/kani_middle/kani_functions.rs
@@ -148,6 +148,8 @@ pub enum KaniHook {
     PointerOffset,
     #[strum(serialize = "SafetyCheckHook")]
     SafetyCheck,
+    #[strum(serialize = "SafetyCheckNoAssumeHook")]
+    SafetyCheckNoAssume,
     #[strum(serialize = "UnsupportedCheckHook")]
     UnsupportedCheck,
     #[strum(serialize = "UntrackedDerefHook")]
diff --git a/kani-compiler/src/kani_middle/transform/body.rs b/kani-compiler/src/kani_middle/transform/body.rs
index f2072fb21fb1..2ead8328e67b 100644
--- a/kani-compiler/src/kani_middle/transform/body.rs
+++ b/kani-compiler/src/kani_middle/transform/body.rs
@@ -181,23 +181,31 @@ impl MutableBody {
         check_type: &CheckType,
         source: &mut SourceInstruction,
         position: InsertPosition,
-        value: Local,
+        value: Option<Local>,
         msg: &str,
     ) {
-        assert_eq!(
-            self.locals[value].ty,
-            Ty::bool_ty(),
-            "Expected boolean value as the assert input"
-        );
         let new_bb = self.blocks.len();
         let span = source.span(&self.blocks);
-        let CheckType::Assert(assert_fn) = check_type;
+        let msg_op = self.new_str_operand(msg, span);
+        let (assert_fn, args) = match check_type {
+            CheckType::SafetyCheck(assert_fn) | CheckType::SafetyCheckNoAssume(assert_fn) => {
+                assert_eq!(
+                    self.locals[value.unwrap()].ty,
+                    Ty::bool_ty(),
+                    "Expected boolean value as the assert input"
+                );
+                (assert_fn, vec![Operand::Move(Place::from(value.unwrap())), msg_op])
+            }
+            CheckType::UnsupportedCheck(assert_fn) => {
+                assert!(value.is_none());
+                (assert_fn, vec![msg_op])
+            }
+        };
         let assert_op =
             Operand::Copy(Place::from(self.new_local(assert_fn.ty(), span, Mutability::Not)));
-        let msg_op = self.new_str_operand(msg, span);
         let kind = TerminatorKind::Call {
             func: assert_op,
-            args: vec![Operand::Move(Place::from(value)), msg_op],
+            args: args,
             destination: Place {
                 local: self.new_local(Ty::new_tuple(&[]), span, Mutability::Not),
                 projection: vec![],
@@ -441,30 +449,35 @@ impl MutableBody {
     }
 }
 
-// TODO: Remove this enum, since we now only support kani's assert.
 #[derive(Clone, Debug)]
 pub enum CheckType {
-    /// This is used by default when the `kani` crate is available.
-    Assert(Instance),
+    SafetyCheck(Instance),
+    SafetyCheckNoAssume(Instance),
+    UnsupportedCheck(Instance),
 }
 
 impl CheckType {
-    /// This will create the type of check that is available in the current crate, attempting to
-    /// create a check that generates an assertion following by an assumption of the same assertion.
-    pub fn new_assert_assume(queries: &QueryDb) -> CheckType {
-        let fn_def = queries.kani_functions()[&KaniHook::Assert.into()];
-        CheckType::Assert(Instance::resolve(fn_def, &GenericArgs(vec![])).unwrap())
-    }
-
-    /// This will create the type of check that is available in the current crate, attempting to
-    /// create a check that generates an assertion, without assuming the condition afterwards.
-    ///
-    /// If `kani` crate is available, this will return [CheckType::Assert], and the instance will
-    /// point to `kani::assert`. Otherwise, we will collect the `core::panic_str` method and return
-    /// [CheckType::Panic].
-    pub fn new_assert(queries: &QueryDb) -> CheckType {
-        let fn_def = queries.kani_functions()[&KaniHook::Check.into()];
-        CheckType::Assert(Instance::resolve(fn_def, &GenericArgs(vec![])).unwrap())
+    /// This will create the type of safety check that is available in the current crate, attempting
+    /// to create a check that generates an assertion following by an assumption of the same
+    /// assertion.
+    pub fn new_safety_check_assert_assume(queries: &QueryDb) -> CheckType {
+        let fn_def = queries.kani_functions()[&KaniHook::SafetyCheck.into()];
+        CheckType::SafetyCheck(Instance::resolve(fn_def, &GenericArgs(vec![])).unwrap())
+    }
+
+    /// This will create the type of safety check that is available in the current crate, attempting
+    /// to create a check that generates an assertion, but not following by an assumption.
+    pub fn new_safety_check_assert_no_assume(queries: &QueryDb) -> CheckType {
+        let fn_def = queries.kani_functions()[&KaniHook::SafetyCheckNoAssume.into()];
+        CheckType::SafetyCheckNoAssume(Instance::resolve(fn_def, &GenericArgs(vec![])).unwrap())
+    }
+
+    /// This will create the type of operation-unsupported check that is available in the current
+    /// crate, attempting to create a check that generates an assertion following by an assumption
+    /// of the same assertion.
+    pub fn new_unsupported_check_assert_assume_false(queries: &QueryDb) -> CheckType {
+        let fn_def = queries.kani_functions()[&KaniHook::UnsupportedCheck.into()];
+        CheckType::UnsupportedCheck(Instance::resolve(fn_def, &GenericArgs(vec![])).unwrap())
     }
 }
 
diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/mod.rs b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/mod.rs
index 19d625da6c53..15d5af1dced6 100644
--- a/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/mod.rs
+++ b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/mod.rs
@@ -33,13 +33,22 @@ mod instrumentation_visitor;
 
 #[derive(Debug)]
 pub struct DelayedUbPass {
-    pub check_type: CheckType,
+    pub safety_check_type: CheckType,
+    pub unsupported_check_type: CheckType,
     pub mem_init_fn_cache: HashMap<KaniFunction, FnDef>,
 }
 
 impl DelayedUbPass {
-    pub fn new(check_type: CheckType, queries: &QueryDb) -> Self {
-        Self { check_type, mem_init_fn_cache: queries.kani_functions().clone() }
+    pub fn new(
+        safety_check_type: CheckType,
+        unsupported_check_type: CheckType,
+        queries: &QueryDb,
+    ) -> Self {
+        Self {
+            safety_check_type,
+            unsupported_check_type,
+            mem_init_fn_cache: queries.kani_functions().clone(),
+        }
     }
 }
 
@@ -122,7 +131,8 @@ impl GlobalPass for DelayedUbPass {
                 let (instrumentation_added, body) = UninitInstrumenter::run(
                     body,
                     instance,
-                    self.check_type.clone(),
+                    self.safety_check_type.clone(),
+                    self.unsupported_check_type.clone(),
                     &mut self.mem_init_fn_cache,
                     target_finder,
                 );
diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs
index 892c2086c65c..e7178e2a7eb0 100644
--- a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs
+++ b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs
@@ -70,7 +70,8 @@ const SKIPPED_ITEMS: &[KaniFunction] = &[
 
 /// Instruments the code with checks for uninitialized memory, agnostic to the source of targets.
 pub struct UninitInstrumenter<'a> {
-    check_type: CheckType,
+    safety_check_type: CheckType,
+    unsupported_check_type: CheckType,
     /// Used to cache FnDef lookups of injected memory initialization functions.
     mem_init_fn_cache: &'a mut HashMap<KaniFunction, FnDef>,
 }
@@ -80,11 +81,13 @@ impl<'a> UninitInstrumenter<'a> {
     pub(crate) fn run(
         body: Body,
         instance: Instance,
-        check_type: CheckType,
+        safety_check_type: CheckType,
+        unsupported_check_type: CheckType,
         mem_init_fn_cache: &'a mut HashMap<KaniFunction, FnDef>,
         target_finder: impl TargetFinder,
     ) -> (bool, Body) {
-        let mut instrumenter = Self { check_type, mem_init_fn_cache };
+        let mut instrumenter =
+            Self { safety_check_type, unsupported_check_type, mem_init_fn_cache };
         let body = MutableBody::from(body);
         let (changed, new_body) = instrumenter.instrument(body, instance, target_finder);
         (changed, new_body.into())
@@ -134,12 +137,11 @@ impl<'a> UninitInstrumenter<'a> {
         source: &mut SourceInstruction,
         operation: MemoryInitOp,
     ) {
-        if let MemoryInitOp::Unsupported { reason } | MemoryInitOp::TriviallyUnsafe { reason } =
-            &operation
-        {
-            // If the operation is unsupported or trivially accesses uninitialized memory, encode
-            // the check as `assert!(false)`.
-            self.inject_assert_false(body, source, operation.position(), reason);
+        if let MemoryInitOp::Unsupported { reason } = &operation {
+            self.inject_unsupported_check(body, source, operation.position(), reason);
+            return;
+        } else if let MemoryInitOp::TriviallyUnsafe { reason } = &operation {
+            self.inject_safety_check(body, source, operation.position(), reason);
             return;
         };
 
@@ -162,7 +164,7 @@ impl<'a> UninitInstrumenter<'a> {
                     let reason = format!(
                         "Kani currently doesn't support checking memory initialization for pointers to `{pointee_ty}. {reason}",
                     );
-                    self.inject_assert_false(body, source, operation.position(), &reason);
+                    self.inject_unsupported_check(body, source, operation.position(), &reason);
                     return;
                 }
             }
@@ -284,7 +286,7 @@ impl<'a> UninitInstrumenter<'a> {
             }
             PointeeLayout::TraitObject => {
                 let reason = "Kani does not support reasoning about memory initialization of pointers to trait objects.";
-                self.inject_assert_false(body, source, operation.position(), reason);
+                self.inject_unsupported_check(body, source, operation.position(), reason);
                 return;
             }
             PointeeLayout::Union { .. } => {
@@ -292,7 +294,7 @@ impl<'a> UninitInstrumenter<'a> {
                 // TODO: we perhaps need to check that the union at least contains an intersection
                 // of all layouts initialized.
                 let reason = "Interaction between raw pointers and unions is not yet supported.";
-                self.inject_assert_false(body, source, operation.position(), reason);
+                self.inject_unsupported_check(body, source, operation.position(), reason);
                 return;
             }
         };
@@ -309,10 +311,10 @@ impl<'a> UninitInstrumenter<'a> {
             _ => unreachable!(),
         };
         body.insert_check(
-            &self.check_type,
+            &self.safety_check_type,
             source,
             operation.position(),
-            ret_place.local,
+            Some(ret_place.local),
             &format!(
                 "Undefined Behavior: Reading from an uninitialized pointer of type `{operand_ty}`"
             ),
@@ -452,7 +454,7 @@ impl<'a> UninitInstrumenter<'a> {
                     None => {
                         let reason =
                             "Interaction between raw pointers and unions is not yet supported.";
-                        self.inject_assert_false(body, source, operation.position(), reason);
+                        self.inject_unsupported_check(body, source, operation.position(), reason);
                         return;
                     }
                 };
@@ -617,7 +619,7 @@ impl<'a> UninitInstrumenter<'a> {
         body.insert_bb(BasicBlock { statements, terminator }, source, operation.position());
     }
 
-    fn inject_assert_false(
+    fn inject_safety_check(
         &self,
         body: &mut MutableBody,
         source: &mut SourceInstruction,
@@ -631,7 +633,17 @@ impl<'a> UninitInstrumenter<'a> {
             user_ty: None,
         }));
         let result = body.insert_assignment(rvalue, source, position);
-        body.insert_check(&self.check_type, source, position, result, reason);
+        body.insert_check(&self.safety_check_type, source, position, Some(result), reason);
+    }
+
+    fn inject_unsupported_check(
+        &self,
+        body: &mut MutableBody,
+        source: &mut SourceInstruction,
+        position: InsertPosition,
+        reason: &str,
+    ) {
+        body.insert_check(&self.unsupported_check_type, source, position, None, reason);
     }
 }
 
diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/mod.rs b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/mod.rs
index b8a8806ec48a..3cba12bf21ee 100644
--- a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/mod.rs
+++ b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/mod.rs
@@ -30,7 +30,8 @@ mod uninit_visitor;
 /// pointers.
 #[derive(Debug)]
 pub struct UninitPass {
-    pub check_type: CheckType,
+    pub safety_check_type: CheckType,
+    pub unsupported_check_type: CheckType,
     pub mem_init_fn_cache: HashMap<KaniFunction, FnDef>,
 }
 
@@ -66,7 +67,8 @@ impl TransformPass for UninitPass {
         let (instrumentation_added, body) = UninitInstrumenter::run(
             new_body.into(),
             instance,
-            self.check_type.clone(),
+            self.safety_check_type.clone(),
+            self.unsupported_check_type.clone(),
             &mut self.mem_init_fn_cache,
             CheckUninitVisitor::new(),
         );
diff --git a/kani-compiler/src/kani_middle/transform/check_values.rs b/kani-compiler/src/kani_middle/transform/check_values.rs
index e2c8a153c9a1..8689bf6c59ac 100644
--- a/kani-compiler/src/kani_middle/transform/check_values.rs
+++ b/kani-compiler/src/kani_middle/transform/check_values.rs
@@ -27,12 +27,12 @@ use stable_mir::abi::{FieldsShape, Scalar, TagEncoding, ValueAbi, VariantsShape,
 use stable_mir::mir::mono::Instance;
 use stable_mir::mir::visit::{Location, PlaceContext, PlaceRef};
 use stable_mir::mir::{
-    AggregateKind, BasicBlockIdx, BinOp, Body, CastKind, ConstOperand, FieldIdx, Local, LocalDecl,
-    MirVisitor, Mutability, NonDivergingIntrinsic, Operand, Place, ProjectionElem, RawPtrKind,
-    Rvalue, Statement, StatementKind, Terminator, TerminatorKind,
+    AggregateKind, BasicBlockIdx, BinOp, Body, CastKind, FieldIdx, Local, LocalDecl, MirVisitor,
+    Mutability, NonDivergingIntrinsic, Operand, Place, ProjectionElem, RawPtrKind, Rvalue,
+    Statement, StatementKind, Terminator, TerminatorKind,
 };
 use stable_mir::target::{MachineInfo, MachineSize};
-use stable_mir::ty::{AdtKind, IndexedVal, MirConst, RigidTy, Span, Ty, TyKind, UintTy};
+use stable_mir::ty::{AdtKind, IndexedVal, RigidTy, Span, Ty, TyKind, UintTy};
 use std::fmt::Debug;
 use strum_macros::AsRefStr;
 use tracing::{debug, trace};
@@ -40,7 +40,8 @@ use tracing::{debug, trace};
 /// Instrument the code with checks for invalid values.
 #[derive(Debug)]
 pub struct ValidValuePass {
-    pub check_type: CheckType,
+    pub safety_check_type: CheckType,
+    pub unsupported_check_type: CheckType,
 }
 
 impl TransformPass for ValidValuePass {
@@ -92,10 +93,10 @@ impl ValidValuePass {
                         let msg =
                             format!("Undefined Behavior: Invalid value of type `{target_ty}`",);
                         body.insert_check(
-                            &self.check_type,
+                            &self.safety_check_type,
                             &mut source,
                             InsertPosition::Before,
-                            result,
+                            Some(result),
                             &msg,
                         );
                     }
@@ -106,10 +107,10 @@ impl ValidValuePass {
                         let msg =
                             format!("Undefined Behavior: Invalid value of type `{pointee_ty}`",);
                         body.insert_check(
-                            &self.check_type,
+                            &self.safety_check_type,
                             &mut source,
                             InsertPosition::Before,
-                            result,
+                            Some(result),
                             &msg,
                         );
                     }
@@ -130,14 +131,13 @@ impl ValidValuePass {
         source: &mut SourceInstruction,
         reason: &str,
     ) {
-        let span = source.span(body.blocks());
-        let rvalue = Rvalue::Use(Operand::Constant(ConstOperand {
-            const_: MirConst::from_bool(false),
-            span,
-            user_ty: None,
-        }));
-        let result = body.insert_assignment(rvalue, source, InsertPosition::Before);
-        body.insert_check(&self.check_type, source, InsertPosition::Before, result, reason);
+        body.insert_check(
+            &self.unsupported_check_type,
+            source,
+            InsertPosition::Before,
+            None,
+            reason,
+        );
     }
 }
 
diff --git a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs
index d18b4b059063..343fc2fe0c92 100644
--- a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs
+++ b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs
@@ -39,7 +39,7 @@ use tracing::{debug, trace};
 /// Generate the body for a few Kani intrinsics.
 #[derive(Debug)]
 pub struct IntrinsicGeneratorPass {
-    check_type: CheckType,
+    unsupported_check_type: CheckType,
     /// Used to cache FnDef lookups for models and Kani intrinsics.
     kani_defs: HashMap<KaniFunction, FnDef>,
     /// Whether the user enabled uninitialized memory checks when they invoked Kani.
@@ -86,11 +86,11 @@ impl TransformPass for IntrinsicGeneratorPass {
 }
 
 impl IntrinsicGeneratorPass {
-    pub fn new(check_type: CheckType, queries: &QueryDb) -> Self {
+    pub fn new(unsupported_check_type: CheckType, queries: &QueryDb) -> Self {
         let enable_uninit = queries.args().ub_check.contains(&ExtraChecks::Uninit);
         let kani_defs = queries.kani_functions().clone();
         debug!(?kani_defs, ?enable_uninit, "IntrinsicGeneratorPass::new");
-        IntrinsicGeneratorPass { check_type, enable_uninit, kani_defs }
+        IntrinsicGeneratorPass { unsupported_check_type, enable_uninit, kani_defs }
     }
 
     /// Generate the body for valid value. Which should be something like:
@@ -151,21 +151,14 @@ impl IntrinsicGeneratorPass {
             }
             Err(msg) => {
                 // We failed to retrieve all the valid ranges.
-                let rvalue = Rvalue::Use(Operand::Constant(ConstOperand {
-                    const_: MirConst::from_bool(false),
-                    span,
-                    user_ty: None,
-                }));
-                let result =
-                    new_body.insert_assignment(rvalue, &mut terminator, InsertPosition::Before);
                 let reason = format!(
                     "Kani currently doesn't support checking validity of `{target_ty}`. {msg}"
                 );
                 new_body.insert_check(
-                    &self.check_type,
+                    &self.unsupported_check_type,
                     &mut terminator,
                     InsertPosition::Before,
-                    result,
+                    None,
                     &reason,
                 );
             }
@@ -314,39 +307,25 @@ impl IntrinsicGeneratorPass {
                         );
                     }
                     PointeeLayout::TraitObject => {
-                        let rvalue = Rvalue::Use(Operand::Constant(ConstOperand {
-                            const_: MirConst::from_bool(false),
-                            span: source.span(new_body.blocks()),
-                            user_ty: None,
-                        }));
-                        let result =
-                            new_body.insert_assignment(rvalue, &mut source, InsertPosition::Before);
                         let reason: &str = "Kani does not support reasoning about memory initialization of pointers to trait objects.";
 
                         new_body.insert_check(
-                            &self.check_type,
+                            &self.unsupported_check_type,
                             &mut source,
                             InsertPosition::Before,
-                            result,
+                            None,
                             &reason,
                         );
                     }
                     PointeeLayout::Union { .. } => {
-                        let rvalue = Rvalue::Use(Operand::Constant(ConstOperand {
-                            const_: MirConst::from_bool(false),
-                            span: source.span(new_body.blocks()),
-                            user_ty: None,
-                        }));
-                        let result =
-                            new_body.insert_assignment(rvalue, &mut source, InsertPosition::Before);
                         let reason: &str =
                             "Kani does not yet support using initialization predicates on unions.";
 
                         new_body.insert_check(
-                            &self.check_type,
+                            &self.unsupported_check_type,
                             &mut source,
                             InsertPosition::Before,
-                            result,
+                            None,
                             &reason,
                         );
                     }
@@ -354,21 +333,14 @@ impl IntrinsicGeneratorPass {
             }
             Err(reason) => {
                 // We failed to retrieve the type layout.
-                let rvalue = Rvalue::Use(Operand::Constant(ConstOperand {
-                    const_: MirConst::from_bool(false),
-                    span: source.span(new_body.blocks()),
-                    user_ty: None,
-                }));
-                let result =
-                    new_body.insert_assignment(rvalue, &mut source, InsertPosition::Before);
                 let reason = format!(
                     "Kani currently doesn't support checking memory initialization for pointers to `{pointee_ty}. {reason}",
                 );
                 new_body.insert_check(
-                    &self.check_type,
+                    &self.unsupported_check_type,
                     &mut source,
                     InsertPosition::Before,
-                    result,
+                    None,
                     &reason,
                 );
             }
diff --git a/kani-compiler/src/kani_middle/transform/mod.rs b/kani-compiler/src/kani_middle/transform/mod.rs
index d1eac474b47a..fbe9bebf42f8 100644
--- a/kani-compiler/src/kani_middle/transform/mod.rs
+++ b/kani-compiler/src/kani_middle/transform/mod.rs
@@ -72,7 +72,8 @@ impl BodyTransformation {
             inst_passes: vec![],
             cache: Default::default(),
         };
-        let check_type = CheckType::new_assert_assume(queries);
+        let safety_check_type = CheckType::new_safety_check_assert_assume(queries);
+        let unsupported_check_type = CheckType::new_unsupported_check_assert_assume_false(queries);
         // This has to come first, since creating harnesses affects later stubbing and contract passes.
         transformer.add_pass(queries, AutomaticHarnessPass::new(unit, queries));
         transformer.add_pass(queries, FnStubPass::new(&unit.stubs));
@@ -81,7 +82,13 @@ impl BodyTransformation {
         // This has to come after the contract pass since we want this to only replace the closure
         // body that is relevant for this harness.
         transformer.add_pass(queries, AnyModifiesPass::new(tcx, queries, &unit));
-        transformer.add_pass(queries, ValidValuePass { check_type: check_type.clone() });
+        transformer.add_pass(
+            queries,
+            ValidValuePass {
+                safety_check_type: safety_check_type.clone(),
+                unsupported_check_type: unsupported_check_type.clone(),
+            },
+        );
         // Putting `UninitPass` after `ValidValuePass` makes sure that the code generated by
         // `UninitPass` does not get unnecessarily instrumented by valid value checks. However, it
         // would also make sense to check that the values are initialized before checking their
@@ -91,11 +98,13 @@ impl BodyTransformation {
             queries,
             UninitPass {
                 // Since this uses demonic non-determinism under the hood, should not assume the assertion.
-                check_type: CheckType::new_assert(queries),
+                safety_check_type: CheckType::new_safety_check_assert_no_assume(queries),
+                unsupported_check_type: unsupported_check_type.clone(),
                 mem_init_fn_cache: queries.kani_functions().clone(),
             },
         );
-        transformer.add_pass(queries, IntrinsicGeneratorPass::new(check_type, &queries));
+        transformer
+            .add_pass(queries, IntrinsicGeneratorPass::new(unsupported_check_type, &queries));
         transformer.add_pass(queries, LoopContractPass::new(tcx, queries, &unit));
         transformer.add_pass(queries, RustcIntrinsicsPass::new(&queries));
         transformer
@@ -198,8 +207,14 @@ pub struct GlobalPasses {
 impl GlobalPasses {
     pub fn new(queries: &QueryDb, tcx: TyCtxt) -> Self {
         let mut global_passes = GlobalPasses { global_passes: vec![] };
-        global_passes
-            .add_global_pass(queries, DelayedUbPass::new(CheckType::new_assert(queries), queries));
+        global_passes.add_global_pass(
+            queries,
+            DelayedUbPass::new(
+                CheckType::new_safety_check_assert_assume(queries),
+                CheckType::new_unsupported_check_assert_assume_false(queries),
+                queries,
+            ),
+        );
         global_passes.add_global_pass(queries, DumpMirPass::new(tcx));
         global_passes
     }
diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs
index d3940160a91a..51b243c9ad33 100644
--- a/library/kani_core/src/lib.rs
+++ b/library/kani_core/src/lib.rs
@@ -358,6 +358,18 @@ macro_rules! kani_intrinsics {
             assert!(cond, "Safety check failed: {msg}");
         }
 
+        #[doc(hidden)]
+        #[allow(dead_code)]
+        #[kanitool::fn_marker = "SafetyCheckNoAssumeHook"]
+        #[inline(never)]
+        pub(crate) fn safety_check_no_assume(cond: bool, msg: &'static str) {
+            #[cfg(not(feature = "concrete_playback"))]
+            return kani_intrinsic();
+
+            #[cfg(feature = "concrete_playback")]
+            assert!(cond, "Safety check failed: {msg}");
+        }
+
         /// This should indicate that Kani does not support a certain operation.
         #[doc(hidden)]
         #[allow(dead_code)]
diff --git a/tests/expected/uninit/access-padding-uninit/access-padding-enum-diverging-variants.expected b/tests/expected/uninit/access-padding-uninit/access-padding-enum-diverging-variants.expected
new file mode 100644
index 000000000000..2d7c3fcccbd3
--- /dev/null
+++ b/tests/expected/uninit/access-padding-uninit/access-padding-enum-diverging-variants.expected
@@ -0,0 +1,5 @@
+ ** 1 of 8 failed\
+Failed Checks: Kani currently doesn't support checking memory initialization for pointers to `E1. Cannot determine layout for an Enum of type E1, as it has multiple variants that have different padding.
+
+Verification failed for - access_padding_unsupported
+Complete - 1 successfully verified harnesses, 1 failures, 2 total.
diff --git a/tests/kani/Uninit/access-padding-enum-diverging-variants.rs b/tests/expected/uninit/access-padding-uninit/access-padding-enum-diverging-variants.rs
similarity index 97%
rename from tests/kani/Uninit/access-padding-enum-diverging-variants.rs
rename to tests/expected/uninit/access-padding-uninit/access-padding-enum-diverging-variants.rs
index fae491c40622..6f41961acb13 100644
--- a/tests/kani/Uninit/access-padding-enum-diverging-variants.rs
+++ b/tests/expected/uninit/access-padding-uninit/access-padding-enum-diverging-variants.rs
@@ -21,7 +21,6 @@ enum E2 {
 }
 
 #[kani::proof]
-#[kani::should_panic]
 fn access_padding_unsupported() {
     let s = E1::A(0, 0);
     let ptr: *const u8 = addr_of!(s) as *const u8;
diff --git a/tests/expected/uninit/access-padding-uninit/access-padding-enum-multiple-variants.expected b/tests/expected/uninit/access-padding-uninit/access-padding-enum-multiple-variants.expected
new file mode 100644
index 000000000000..189fe3ac07c2
--- /dev/null
+++ b/tests/expected/uninit/access-padding-uninit/access-padding-enum-multiple-variants.expected
@@ -0,0 +1,9 @@
+ ** 1 of 32 failed\
+Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u8`
+
+ ** 1 of 32 failed\
+Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u8`
+
+Verification failed for - access_padding_uninit_b
+Verification failed for - access_padding_uninit_a
+Complete - 2 successfully verified harnesses, 2 failures, 4 total.
diff --git a/tests/kani/Uninit/access-padding-enum-multiple-variants.rs b/tests/expected/uninit/access-padding-uninit/access-padding-enum-multiple-variants.rs
similarity index 96%
rename from tests/kani/Uninit/access-padding-enum-multiple-variants.rs
rename to tests/expected/uninit/access-padding-uninit/access-padding-enum-multiple-variants.rs
index dd6942252cb2..11c70dd7cd92 100644
--- a/tests/kani/Uninit/access-padding-enum-multiple-variants.rs
+++ b/tests/expected/uninit/access-padding-uninit/access-padding-enum-multiple-variants.rs
@@ -33,7 +33,6 @@ fn access_padding_init_b() {
 }
 
 #[kani::proof]
-#[kani::should_panic]
 fn access_padding_uninit_a() {
     let s = E::A(0, 0);
     let ptr: *const u8 = addr_of!(s) as *const u8;
@@ -41,7 +40,6 @@ fn access_padding_uninit_a() {
 }
 
 #[kani::proof]
-#[kani::should_panic]
 fn access_padding_uninit_b() {
     let s = E::A(0, 0);
     let ptr: *const u8 = addr_of!(s) as *const u8;
diff --git a/tests/expected/uninit/access-padding-uninit/access-padding-enum-single-field.expected b/tests/expected/uninit/access-padding-uninit/access-padding-enum-single-field.expected
new file mode 100644
index 000000000000..a93c98c4b00a
--- /dev/null
+++ b/tests/expected/uninit/access-padding-uninit/access-padding-enum-single-field.expected
@@ -0,0 +1,6 @@
+ ** 2 of 40 failed\
+Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u8`
+Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u8`
+
+Verification failed for - access_padding_uninit
+Complete - 1 successfully verified harnesses, 1 failures, 2 total.
diff --git a/tests/kani/Uninit/access-padding-enum-single-field.rs b/tests/expected/uninit/access-padding-uninit/access-padding-enum-single-field.rs
similarity index 97%
rename from tests/kani/Uninit/access-padding-enum-single-field.rs
rename to tests/expected/uninit/access-padding-uninit/access-padding-enum-single-field.rs
index 63f7f6043905..da1f2a202364 100644
--- a/tests/kani/Uninit/access-padding-enum-single-field.rs
+++ b/tests/expected/uninit/access-padding-uninit/access-padding-enum-single-field.rs
@@ -25,7 +25,6 @@ fn access_padding_init() {
 }
 
 #[kani::proof]
-#[kani::should_panic]
 fn access_padding_uninit() {
     let s = E::A(0);
     let ptr: *const u8 = addr_of!(s) as *const u8;
diff --git a/tests/expected/uninit/access-padding-uninit/access-padding-enum-single-variant.expected b/tests/expected/uninit/access-padding-uninit/access-padding-enum-single-variant.expected
new file mode 100644
index 000000000000..690217c15a38
--- /dev/null
+++ b/tests/expected/uninit/access-padding-uninit/access-padding-enum-single-variant.expected
@@ -0,0 +1,5 @@
+ ** 1 of 32 failed\
+Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u8`
+
+Verification failed for - access_padding_uninit
+Complete - 1 successfully verified harnesses, 1 failures, 2 total.
diff --git a/tests/kani/Uninit/access-padding-enum-single-variant.rs b/tests/expected/uninit/access-padding-uninit/access-padding-enum-single-variant.rs
similarity index 97%
rename from tests/kani/Uninit/access-padding-enum-single-variant.rs
rename to tests/expected/uninit/access-padding-uninit/access-padding-enum-single-variant.rs
index bb87d36d26c8..9946fc83cee9 100644
--- a/tests/kani/Uninit/access-padding-enum-single-variant.rs
+++ b/tests/expected/uninit/access-padding-uninit/access-padding-enum-single-variant.rs
@@ -24,7 +24,6 @@ fn access_padding_init() {
 }
 
 #[kani::proof]
-#[kani::should_panic]
 fn access_padding_uninit() {
     let s = E::A(0, 0);
     let ptr: *const u8 = addr_of!(s) as *const u8;
diff --git a/tests/expected/uninit/access-padding-uninit/expected b/tests/expected/uninit/access-padding-uninit/access-padding-uninit.expected
similarity index 100%
rename from tests/expected/uninit/access-padding-uninit/expected
rename to tests/expected/uninit/access-padding-uninit/access-padding-uninit.expected
diff --git a/tests/expected/valid-value-checks/constants.expected b/tests/expected/valid-value-checks/constants.expected
new file mode 100644
index 000000000000..01b2cdb529d8
--- /dev/null
+++ b/tests/expected/valid-value-checks/constants.expected
@@ -0,0 +1,13 @@
+ ** 1 of 22 failed\
+Failed Checks: Undefined Behavior: Invalid value of type `[char; 2]`
+
+ ** 1 of 15 failed\
+Failed Checks: Undefined Behavior: Invalid value of type `char`
+
+ ** 1 of 3 failed\
+Failed Checks: Undefined Behavior: Invalid value of type `bool`
+
+Verification failed for - cast_to_invalid_offset
+Verification failed for - cast_to_invalid_char
+Verification failed for - transmute_invalid_bool
+Complete - 3 successfully verified harnesses, 3 failures, 6 total.
diff --git a/tests/kani/ValidValues/constants.rs b/tests/expected/valid-value-checks/constants.rs
similarity index 93%
rename from tests/kani/ValidValues/constants.rs
rename to tests/expected/valid-value-checks/constants.rs
index 5230e6e5e6cb..aa7aba6fe079 100644
--- a/tests/kani/ValidValues/constants.rs
+++ b/tests/expected/valid-value-checks/constants.rs
@@ -21,19 +21,16 @@ fn cast_to_valid_offset() {
 }
 
 #[kani::proof]
-#[kani::should_panic]
 fn transmute_invalid_bool() {
     let _b = unsafe { std::mem::transmute::<u8, bool>(2) };
 }
 
 #[kani::proof]
-#[kani::should_panic]
 fn cast_to_invalid_char() {
     let _c = unsafe { *(&u32::MAX as *const u32 as *const char) };
 }
 
 #[kani::proof]
-#[kani::should_panic]
 fn cast_to_invalid_offset() {
     let val = [100u32, u32::MAX];
     let _c = unsafe { *(&val as *const [u32; 2] as *const [char; 2]) };
diff --git a/tests/expected/valid-value-checks/custom_niche.expected b/tests/expected/valid-value-checks/custom_niche.expected
new file mode 100644
index 000000000000..5a5a8d03e541
--- /dev/null
+++ b/tests/expected/valid-value-checks/custom_niche.expected
@@ -0,0 +1,37 @@
+ ** 1 of 19 failed\
+Failed Checks: Undefined Behavior: Invalid value of type `Rating`
+
+ ** 1 of 33 failed (4 unreachable)\
+Failed Checks: Kani currently doesn't support checking validity of `copy_nonoverlapping` for `*const Rating`
+
+ ** 1 of 45 failed (4 unreachable)\
+Failed Checks: Kani currently doesn't support checking validity of `copy_nonoverlapping` for `*const Rating`
+
+ ** 1 of 33 failed (4 unreachable)\
+Failed Checks: Undefined Behavior: Invalid value of type `Rating`
+
+ ** 1 of 3 failed\
+Failed Checks: Undefined Behavior: Invalid value of type `Rating`
+
+ ** 1 of 15 failed\
+Failed Checks: Undefined Behavior: Invalid value of type `Rating`
+
+ ** 1 of 16 failed\
+Failed Checks: Undefined Behavior: Invalid value of type `Rating`
+
+ ** 1 of 4 failed\
+Failed Checks: Undefined Behavior: Invalid value of type `Rating`
+
+ ** 1 of 36 failed (1 unreachable)\
+Failed Checks: Undefined Behavior: Invalid value of type `Rating`
+
+Verification failed for - check_invalid_increment
+Verification failed for - check_copy_nonoverlap_ub
+Verification failed for - check_copy_nonoverlap
+Verification failed for - check_invalid_transmute_copy
+Verification failed for - check_invalid_transmute
+Verification failed for - check_invalid_dereference
+Verification failed for - check_new_with_ub_limits
+Verification failed for - check_unchecked_new_ub
+Verification failed for - check_new_with_ub
+Complete - 2 successfully verified harnesses, 9 failures, 11 total.
diff --git a/tests/kani/ValidValues/custom_niche.rs b/tests/expected/valid-value-checks/custom_niche.rs
similarity index 94%
rename from tests/kani/ValidValues/custom_niche.rs
rename to tests/expected/valid-value-checks/custom_niche.rs
index b282fec3c645..c27bc6fdc057 100644
--- a/tests/kani/ValidValues/custom_niche.rs
+++ b/tests/expected/valid-value-checks/custom_niche.rs
@@ -38,41 +38,35 @@ impl Rating {
 }
 
 #[kani::proof]
-#[kani::should_panic]
 pub fn check_new_with_ub() {
     assert_eq!(Rating::new(10), None);
 }
 
 #[kani::proof]
-#[kani::should_panic]
 pub fn check_unchecked_new_ub() {
     let val = kani::any();
     assert_eq!(unsafe { Rating::new_unchecked(val).stars }, val);
 }
 
 #[kani::proof]
-#[kani::should_panic]
 pub fn check_new_with_ub_limits() {
     let stars = kani::any_where(|s: &u8| *s == 0 || *s > 5);
     let _ = Rating::new(stars);
 }
 
 #[kani::proof]
-#[kani::should_panic]
 pub fn check_invalid_dereference() {
     let any: u8 = kani::any();
     let _rating: Rating = unsafe { *(&any as *const _ as *const _) };
 }
 
 #[kani::proof]
-#[kani::should_panic]
 pub fn check_invalid_transmute() {
     let any: u8 = kani::any();
     let _rating: Rating = unsafe { mem::transmute(any) };
 }
 
 #[kani::proof]
-#[kani::should_panic]
 pub fn check_invalid_transmute_copy() {
     let any: u8 = kani::any();
     let _rating: Rating = unsafe { mem::transmute_copy(&any) };
@@ -82,7 +76,6 @@ pub fn check_invalid_transmute_copy() {
 ///
 /// FIX-ME: This is not supported today, and we fail due to unsupported check.
 #[kani::proof]
-#[kani::should_panic]
 pub fn check_copy_nonoverlap() {
     let stars = kani::any_where(|s: &u8| *s == 0 || *s > 5);
     let mut rating: Rating = kani::any();
@@ -90,7 +83,6 @@ pub fn check_copy_nonoverlap() {
 }
 
 #[kani::proof]
-#[kani::should_panic]
 pub fn check_copy_nonoverlap_ub() {
     let any: u8 = kani::any();
     let mut rating: Rating = kani::any();
@@ -98,7 +90,6 @@ pub fn check_copy_nonoverlap_ub() {
 }
 
 #[kani::proof]
-#[kani::should_panic]
 pub fn check_invalid_increment() {
     let mut orig: Rating = kani::any();
     unsafe { orig.stars += 1 };
diff --git a/tests/expected/valid-value-checks/maybe_uninit.expected b/tests/expected/valid-value-checks/maybe_uninit.expected
new file mode 100644
index 000000000000..8264876dc4f7
--- /dev/null
+++ b/tests/expected/valid-value-checks/maybe_uninit.expected
@@ -0,0 +1,5 @@
+ ** 1 of 14 failed (1 unreachable)\
+Failed Checks: Undefined Behavior: Invalid value of type `std::num::NonZero<i64>`
+
+Verification failed for - check_invalid_zeroed
+Complete - 1 successfully verified harnesses, 1 failures, 2 total.
diff --git a/tests/kani/ValidValues/maybe_uninit.rs b/tests/expected/valid-value-checks/maybe_uninit.rs
similarity index 96%
rename from tests/kani/ValidValues/maybe_uninit.rs
rename to tests/expected/valid-value-checks/maybe_uninit.rs
index 620ad8ef5ba3..926277a744dc 100644
--- a/tests/kani/ValidValues/maybe_uninit.rs
+++ b/tests/expected/valid-value-checks/maybe_uninit.rs
@@ -14,7 +14,6 @@ pub fn check_valid_zeroed() {
 }
 
 #[kani::proof]
-#[kani::should_panic]
 pub fn check_invalid_zeroed() {
     let maybe = MaybeUninit::zeroed();
     let _val: NonZeroI64 = unsafe { maybe.assume_init() };
diff --git a/tests/expected/valid-value-checks/non_null.expected b/tests/expected/valid-value-checks/non_null.expected
new file mode 100644
index 000000000000..110fbf20a4c8
--- /dev/null
+++ b/tests/expected/valid-value-checks/non_null.expected
@@ -0,0 +1,9 @@
+ ** 1 of 39 failed (1 unreachable)\
+Failed Checks: Undefined Behavior: Invalid value of type `std::ptr::NonNull<u8>`
+
+ ** 1 of 6 failed\
+Failed Checks: Undefined Behavior: Invalid value of type `std::ptr::NonNull<u8>`
+
+Verification failed for - check_invalid_value_cfg
+Verification failed for - check_invalid_value
+Complete - 1 successfully verified harnesses, 2 failures, 3 total.
diff --git a/tests/kani/ValidValues/non_null.rs b/tests/expected/valid-value-checks/non_null.rs
similarity index 94%
rename from tests/kani/ValidValues/non_null.rs
rename to tests/expected/valid-value-checks/non_null.rs
index 4874b61bf2d0..85d1a3876785 100644
--- a/tests/kani/ValidValues/non_null.rs
+++ b/tests/expected/valid-value-checks/non_null.rs
@@ -7,13 +7,11 @@ use std::num::NonZeroU8;
 use std::ptr::{self, NonNull};
 
 #[kani::proof]
-#[kani::should_panic]
 pub fn check_invalid_value() {
     let _ = unsafe { NonNull::new_unchecked(ptr::null_mut::<u8>()) };
 }
 
 #[kani::proof]
-#[kani::should_panic]
 pub fn check_invalid_value_cfg() {
     let nn = unsafe { NonNull::new_unchecked(ptr::null_mut::<u8>()) };
     // This should be unreachable. TODO: Make this expected test.
diff --git a/tests/expected/valid-value-checks/write_bytes.expected b/tests/expected/valid-value-checks/write_bytes.expected
new file mode 100644
index 000000000000..8c14a9046d8d
--- /dev/null
+++ b/tests/expected/valid-value-checks/write_bytes.expected
@@ -0,0 +1,5 @@
+ ** 1 of 11 failed (1 unreachable)\
+Failed Checks: Undefined Behavior: Invalid value of type `char`
+
+Verification failed for - check_invalid_write
+Complete - 1 successfully verified harnesses, 1 failures, 2 total.
diff --git a/tests/kani/ValidValues/write_bytes.rs b/tests/expected/valid-value-checks/write_bytes.rs
similarity index 96%
rename from tests/kani/ValidValues/write_bytes.rs
rename to tests/expected/valid-value-checks/write_bytes.rs
index e4f73b1f3479..0b0ae6f343db 100644
--- a/tests/kani/ValidValues/write_bytes.rs
+++ b/tests/expected/valid-value-checks/write_bytes.rs
@@ -5,7 +5,6 @@
 #![feature(core_intrinsics)]
 
 #[kani::proof]
-#[kani::should_panic]
 pub fn check_invalid_write() {
     let mut val = 'a';
     let ptr = &mut val as *mut char;
diff --git a/tests/expected/valid-value-checks/write_invalid.expected b/tests/expected/valid-value-checks/write_invalid.expected
new file mode 100644
index 000000000000..ba6c5b2ba65c
--- /dev/null
+++ b/tests/expected/valid-value-checks/write_invalid.expected
@@ -0,0 +1,13 @@
+ ** 1 of 19 failed (2 unreachable)\
+Failed Checks: Kani currently doesn't support checking validity of `transmute` for `std::option::Option<std::num::NonZero<u8>>`
+
+ ** 1 of 43 failed (2 unreachable)\
+Failed Checks: Kani currently doesn't support checking validity of `transmute` for `std::option::Option<std::num::NonZero<u8>>`
+
+ ** 1 of 18 failed (1 unreachable)\
+Failed Checks: Kani currently doesn't support checking validity of `transmute` for `std::option::Option<std::num::NonZero<u8>>`
+
+Verification failed for - read_invalid_is_ub
+Verification failed for - write_valid_before_read
+Verification failed for - write_invalid_bytes_no_ub_with_spurious_cex
+Complete - 0 successfully verified harnesses, 3 failures, 3 total.
diff --git a/tests/kani/ValidValues/write_invalid.rs b/tests/expected/valid-value-checks/write_invalid.rs
similarity index 94%
rename from tests/kani/ValidValues/write_invalid.rs
rename to tests/expected/valid-value-checks/write_invalid.rs
index 05d3705bd69a..677ffe4edf61 100644
--- a/tests/kani/ValidValues/write_invalid.rs
+++ b/tests/expected/valid-value-checks/write_invalid.rs
@@ -9,7 +9,6 @@
 use std::num::NonZeroU8;
 
 #[kani::proof]
-#[kani::should_panic]
 pub fn write_invalid_bytes_no_ub_with_spurious_cex() {
     let mut non_zero: NonZeroU8 = kani::any();
     let dest = &mut non_zero as *mut _;
@@ -17,7 +16,6 @@ pub fn write_invalid_bytes_no_ub_with_spurious_cex() {
 }
 
 #[kani::proof]
-#[kani::should_panic]
 pub fn write_valid_before_read() {
     let mut non_zero: NonZeroU8 = kani::any();
     let mut non_zero_2: NonZeroU8 = kani::any();
@@ -28,7 +26,6 @@ pub fn write_valid_before_read() {
 }
 
 #[kani::proof]
-#[kani::should_panic]
 pub fn read_invalid_is_ub() {
     let mut non_zero: NonZeroU8 = kani::any();
     let dest = &mut non_zero as *mut _;

From dba50e6ccbd255e575c2693ae8f60b9744e52708 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 12 Feb 2025 22:58:03 +0000
Subject: [PATCH 05/10] Fixup tests

---
 .../copy/expose_padding_via_copy.expected     |  4 ++--
 ...xpose_padding_via_copy_convoluted.expected |  4 ++--
 .../expose_padding_via_non_byte_copy.expected |  4 ++--
 .../uninit/copy/read_after_copy.expected      |  4 ++--
 .../uninit/delayed-ub/delayed-ub.expected     | 20 +++++++++----------
 tests/expected/uninit/intrinsics/expected     | 20 ++++++++-----------
 .../uninit/multiple-instrumentations.expected |  8 ++++----
 tests/expected/uninit/unions.expected         | 14 ++++++-------
 8 files changed, 37 insertions(+), 41 deletions(-)

diff --git a/tests/expected/uninit/copy/expose_padding_via_copy.expected b/tests/expected/uninit/copy/expose_padding_via_copy.expected
index 83d8badc8bf5..28686a566df4 100644
--- a/tests/expected/uninit/copy/expose_padding_via_copy.expected
+++ b/tests/expected/uninit/copy/expose_padding_via_copy.expected
@@ -1,8 +1,8 @@
-std::ptr::read::<u64>.assertion.1\
+std::ptr::read::<u64>.safety_check.\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*const u64`"\
 
-std::ptr::read::<u64>.assertion.2\
+std::ptr::read::<u64>.safety_check.\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u64`"\
 
diff --git a/tests/expected/uninit/copy/expose_padding_via_copy_convoluted.expected b/tests/expected/uninit/copy/expose_padding_via_copy_convoluted.expected
index cbe7ec97cb7b..b9cdd6137592 100644
--- a/tests/expected/uninit/copy/expose_padding_via_copy_convoluted.expected
+++ b/tests/expected/uninit/copy/expose_padding_via_copy_convoluted.expected
@@ -1,8 +1,8 @@
-std::ptr::read::<u64>.assertion.1\
+std::ptr::read::<u64>.safety_check.\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*const u64`"\
 
-std::ptr::read::<u64>.assertion.2\
+std::ptr::read::<u64>.safety_check.\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u64`"\
 
diff --git a/tests/expected/uninit/copy/expose_padding_via_non_byte_copy.expected b/tests/expected/uninit/copy/expose_padding_via_non_byte_copy.expected
index 3fc86e45a46e..d3b1db9bd498 100644
--- a/tests/expected/uninit/copy/expose_padding_via_non_byte_copy.expected
+++ b/tests/expected/uninit/copy/expose_padding_via_non_byte_copy.expected
@@ -1,8 +1,8 @@
-std::ptr::read::<u64>.assertion.1\
+std::ptr::read::<u64>.safety_check.\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*const u64`"\
 
-std::ptr::read::<u64>.assertion.2\
+std::ptr::read::<u64>.safety_check.\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u64`"\
 
diff --git a/tests/expected/uninit/copy/read_after_copy.expected b/tests/expected/uninit/copy/read_after_copy.expected
index 56a3460a1d7b..c5d133d787b9 100644
--- a/tests/expected/uninit/copy/read_after_copy.expected
+++ b/tests/expected/uninit/copy/read_after_copy.expected
@@ -1,8 +1,8 @@
-std::ptr::read::<u64>.assertion.1\
+std::ptr::read::<u64>.safety_check.\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*const u64`"\
 
-std::ptr::read::<u64>.assertion.2\
+std::ptr::read::<u64>.safety_check.\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u64`"\
 
diff --git a/tests/expected/uninit/delayed-ub/delayed-ub.expected b/tests/expected/uninit/delayed-ub/delayed-ub.expected
index f062a30cf6b0..d998801c2ca7 100644
--- a/tests/expected/uninit/delayed-ub/delayed-ub.expected
+++ b/tests/expected/uninit/delayed-ub/delayed-ub.expected
@@ -1,40 +1,40 @@
-delayed_ub_trigger_copy.assertion.\
+delayed_ub_trigger_copy.safety_check.\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"\
 
-delayed_ub_structs.assertion.\
+delayed_ub_structs.safety_check.\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `U`"
 
-delayed_ub_double_copy.assertion.\
+delayed_ub_double_copy.safety_check.\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"\
 
-delayed_ub_copy.assertion.\
+delayed_ub_copy.safety_check.\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"
 
-delayed_ub_closure_capture_laundered.assertion.\
+delayed_ub_closure_capture_laundered.safety_check.\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"
 
-delayed_ub_closure_laundered.assertion.\
+delayed_ub_closure_laundered.safety_check.\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"
 
-delayed_ub_laundered.assertion.\
+delayed_ub_laundered.safety_check.\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"
 
-delayed_ub_static.assertion.\
+delayed_ub_static.safety_check.\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"
 
-delayed_ub_transmute.assertion.\
+delayed_ub_transmute.safety_check.\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"
 
-delayed_ub.assertion.\
+delayed_ub.safety_check.\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"
 
diff --git a/tests/expected/uninit/intrinsics/expected b/tests/expected/uninit/intrinsics/expected
index b40fe6714ba8..d19d694df75e 100644
--- a/tests/expected/uninit/intrinsics/expected
+++ b/tests/expected/uninit/intrinsics/expected
@@ -1,36 +1,32 @@
-std::ptr::write::<std::mem::MaybeUninit<u8>>.assertion.1\
+std::ptr::read::<std::mem::MaybeUninit<u8>>.unsupported_construct.\
 	 - Status: FAILURE\
 	 - Description: "Interaction between raw pointers and unions is not yet supported."
 
-std::ptr::write::<std::mem::MaybeUninit<u8>>.assertion.1\
-	 - Status: FAILURE\
-	 - Description: "Interaction between raw pointers and unions is not yet supported."\
-
-check_typed_swap_nonoverlapping.assertion.1\
+check_typed_swap_nonoverlapping.safety_check.\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*mut u8`"
 
-check_typed_swap_nonoverlapping.assertion.2\
+check_typed_swap_nonoverlapping.safety_check.\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*mut u8`"
 
-check_volatile_load.assertion.1\
+check_volatile_load.safety_check.\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*const u8`"
 
-check_compare_bytes.assertion.1\
+check_compare_bytes.safety_check.\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*const u8`"
 
-check_compare_bytes.assertion.2\
+check_compare_bytes.safety_check.\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*const u8`"
 
-std::ptr::read::<u8>.assertion.1\
+std::ptr::read::<u8>.safety_check.\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*const u8`"
 
-std::ptr::read::<u8>.assertion.2\
+std::ptr::read::<u8>.safety_check.\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u8`"
 
diff --git a/tests/expected/uninit/multiple-instrumentations.expected b/tests/expected/uninit/multiple-instrumentations.expected
index 0f503b624ca4..82f37b22ed0d 100644
--- a/tests/expected/uninit/multiple-instrumentations.expected
+++ b/tests/expected/uninit/multiple-instrumentations.expected
@@ -1,16 +1,16 @@
-multiple_instrumentations_different_vars.assertion\
+multiple_instrumentations_different_vars.safety_check\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"
 
-multiple_instrumentations_different_vars.assertion\
+multiple_instrumentations_different_vars.safety_check\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u64`"
 
-multiple_instrumentations.assertion\
+multiple_instrumentations.safety_check\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"
 
-multiple_instrumentations.assertion\
+multiple_instrumentations.safety_check\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"
 
diff --git a/tests/expected/uninit/unions.expected b/tests/expected/uninit/unions.expected
index ca7f777c4065..cf40fbb608df 100644
--- a/tests/expected/uninit/unions.expected
+++ b/tests/expected/uninit/unions.expected
@@ -1,28 +1,28 @@
-union_update_should_fail.assertion.1\
+union_update_should_fail.safety_check.\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u32`"
 
-union_complex_subfields_should_fail.assertion.1\
+union_complex_subfields_should_fail.safety_check.\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u16`"
 
-basic_union_should_fail.assertion.1\
+basic_union_should_fail.safety_check.\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u32`"
 
-cross_function_union_should_fail::helper.assertion.1\
+cross_function_union_should_fail::helper.safety_check.\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u32`"
 
-cross_function_multi_union_should_fail::helper.assertion.1\
+cross_function_multi_union_should_fail::helper.safety_check.\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u32`"
 
-multi_cross_function_union_should_fail::sub_helper.assertion.1\
+multi_cross_function_union_should_fail::sub_helper.safety_check.\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u32`"
 
-basic_multifield_union_should_fail.assertion.7\
+basic_multifield_union_should_fail.safety_check.\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"
 

From 0f5379cefe852288454a70a69691a2ab3ced3ce0 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Thu, 13 Feb 2025 00:32:27 +0000
Subject: [PATCH 06/10] fixup! Adjust PropertyClass of assertions to identify
 UB

---
 .../codegen/statement.rs                      | 46 ++++++++++++-------
 1 file changed, 29 insertions(+), 17 deletions(-)

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
index b2b023df881b..3e8ac4cf02fb 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
@@ -251,25 +251,37 @@ impl GotocCtx<'_> {
                     if *expected { r } else { Expr::not(r) }
                 };
 
-                let (msg, property_class) = if let AssertMessage::BoundsCheck { .. } = msg {
-                    // For bounds check the following panic message is generated at runtime:
-                    // "index out of bounds: the length is {len} but the index is {index}",
-                    // but CBMC only accepts static messages so we don't add values to the message.
-                    (
-                        "index out of bounds: the length is less than or equal to the given index",
-                        PropertyClass::Assertion,
-                    )
-                } else if let AssertMessage::MisalignedPointerDereference { .. } = msg {
-                    // Misaligned pointer dereference check messages is also a runtime messages.
-                    // Generate a generic one here.
-                    (
-                        "misaligned pointer dereference: address must be a multiple of its type's \
+                let (msg, property_class) = match msg {
+                    AssertMessage::BoundsCheck { .. } => {
+                        // For bounds check the following panic message is generated at runtime:
+                        // "index out of bounds: the length is {len} but the index is {index}",
+                        // but CBMC only accepts static messages so we don't add values to the message.
+                        (
+                            "index out of bounds: the length is less than or equal to the given index",
+                            PropertyClass::Assertion,
+                        )
+                    }
+                    AssertMessage::MisalignedPointerDereference { .. } => {
+                        // Misaligned pointer dereference check messages is also a runtime messages.
+                        // Generate a generic one here.
+                        (
+                            "misaligned pointer dereference: address must be a multiple of its type's \
                     alignment",
-                        PropertyClass::SafetyCheck,
-                    )
-                } else {
+                            PropertyClass::SafetyCheck,
+                        )
+                    }
                     // For all other assert kind we can get the static message.
-                    (msg.description().unwrap(), PropertyClass::Assertion)
+                    AssertMessage::NullPointerDereference { .. } => {
+                        (msg.description().unwrap(), PropertyClass::SafetyCheck)
+                    }
+                    AssertMessage::Overflow { .. }
+                    | AssertMessage::OverflowNeg { .. }
+                    | AssertMessage::DivisionByZero { .. }
+                    | AssertMessage::RemainderByZero { .. }
+                    | AssertMessage::ResumedAfterReturn { .. }
+                    | AssertMessage::ResumedAfterPanic { .. } => {
+                        (msg.description().unwrap(), PropertyClass::Assertion)
+                    }
                 };
 
                 let (msg_str, reach_stmt) =

From 0cf1798672c61408ce2f71f0c5d10da708b4307e Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Thu, 13 Feb 2025 00:57:26 +0000
Subject: [PATCH 07/10] Clippy

---
 kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs | 2 +-
 kani-compiler/src/kani_middle/transform/body.rs              | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
index 3e8ac4cf02fb..813e07d06723 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
@@ -271,7 +271,7 @@ impl GotocCtx<'_> {
                         )
                     }
                     // For all other assert kind we can get the static message.
-                    AssertMessage::NullPointerDereference { .. } => {
+                    AssertMessage::NullPointerDereference => {
                         (msg.description().unwrap(), PropertyClass::SafetyCheck)
                     }
                     AssertMessage::Overflow { .. }
diff --git a/kani-compiler/src/kani_middle/transform/body.rs b/kani-compiler/src/kani_middle/transform/body.rs
index 2ead8328e67b..6f7b59041d12 100644
--- a/kani-compiler/src/kani_middle/transform/body.rs
+++ b/kani-compiler/src/kani_middle/transform/body.rs
@@ -205,7 +205,7 @@ impl MutableBody {
             Operand::Copy(Place::from(self.new_local(assert_fn.ty(), span, Mutability::Not)));
         let kind = TerminatorKind::Call {
             func: assert_op,
-            args: args,
+            args,
             destination: Place {
                 local: self.new_local(Ty::new_tuple(&[]), span, Mutability::Not),
                 projection: vec![],

From e711bb8ac745839fa6e9491f14ccd60601184877 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <mt@debian.org>
Date: Tue, 18 Feb 2025 11:28:48 +0100
Subject: [PATCH 08/10] Apply suggestions from code review

Co-authored-by: Carolyn Zech <cmzech@amazon.com>
---
 .../access-padding-enum-diverging-variants.expected             | 1 -
 .../access-padding-enum-multiple-variants.expected              | 2 --
 .../access-padding-enum-single-field.expected                   | 1 -
 .../access-padding-enum-single-variant.expected                 | 1 -
 4 files changed, 5 deletions(-)

diff --git a/tests/expected/uninit/access-padding-uninit/access-padding-enum-diverging-variants.expected b/tests/expected/uninit/access-padding-uninit/access-padding-enum-diverging-variants.expected
index 2d7c3fcccbd3..89a3572de316 100644
--- a/tests/expected/uninit/access-padding-uninit/access-padding-enum-diverging-variants.expected
+++ b/tests/expected/uninit/access-padding-uninit/access-padding-enum-diverging-variants.expected
@@ -1,4 +1,3 @@
- ** 1 of 8 failed\
 Failed Checks: Kani currently doesn't support checking memory initialization for pointers to `E1. Cannot determine layout for an Enum of type E1, as it has multiple variants that have different padding.
 
 Verification failed for - access_padding_unsupported
diff --git a/tests/expected/uninit/access-padding-uninit/access-padding-enum-multiple-variants.expected b/tests/expected/uninit/access-padding-uninit/access-padding-enum-multiple-variants.expected
index 189fe3ac07c2..29fa17a972f5 100644
--- a/tests/expected/uninit/access-padding-uninit/access-padding-enum-multiple-variants.expected
+++ b/tests/expected/uninit/access-padding-uninit/access-padding-enum-multiple-variants.expected
@@ -1,7 +1,5 @@
- ** 1 of 32 failed\
 Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u8`
 
- ** 1 of 32 failed\
 Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u8`
 
 Verification failed for - access_padding_uninit_b
diff --git a/tests/expected/uninit/access-padding-uninit/access-padding-enum-single-field.expected b/tests/expected/uninit/access-padding-uninit/access-padding-enum-single-field.expected
index a93c98c4b00a..caab803ad09a 100644
--- a/tests/expected/uninit/access-padding-uninit/access-padding-enum-single-field.expected
+++ b/tests/expected/uninit/access-padding-uninit/access-padding-enum-single-field.expected
@@ -1,4 +1,3 @@
- ** 2 of 40 failed\
 Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u8`
 Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u8`
 
diff --git a/tests/expected/uninit/access-padding-uninit/access-padding-enum-single-variant.expected b/tests/expected/uninit/access-padding-uninit/access-padding-enum-single-variant.expected
index 690217c15a38..fa661dfbe329 100644
--- a/tests/expected/uninit/access-padding-uninit/access-padding-enum-single-variant.expected
+++ b/tests/expected/uninit/access-padding-uninit/access-padding-enum-single-variant.expected
@@ -1,4 +1,3 @@
- ** 1 of 32 failed\
 Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u8`
 
 Verification failed for - access_padding_uninit

From bf732079eba3bddbcf2d76083ccecc09603ce54e Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 18 Feb 2025 10:31:30 +0000
Subject: [PATCH 09/10] Further review-feedback application

---
 tests/expected/valid-value-checks/constants.expected    | 3 ---
 tests/expected/valid-value-checks/custom_niche.expected | 9 ---------
 tests/expected/valid-value-checks/non_null.expected     | 2 --
 3 files changed, 14 deletions(-)

diff --git a/tests/expected/valid-value-checks/constants.expected b/tests/expected/valid-value-checks/constants.expected
index 01b2cdb529d8..639e193bc561 100644
--- a/tests/expected/valid-value-checks/constants.expected
+++ b/tests/expected/valid-value-checks/constants.expected
@@ -1,10 +1,7 @@
- ** 1 of 22 failed\
 Failed Checks: Undefined Behavior: Invalid value of type `[char; 2]`
 
- ** 1 of 15 failed\
 Failed Checks: Undefined Behavior: Invalid value of type `char`
 
- ** 1 of 3 failed\
 Failed Checks: Undefined Behavior: Invalid value of type `bool`
 
 Verification failed for - cast_to_invalid_offset
diff --git a/tests/expected/valid-value-checks/custom_niche.expected b/tests/expected/valid-value-checks/custom_niche.expected
index 5a5a8d03e541..3d78563ef8b1 100644
--- a/tests/expected/valid-value-checks/custom_niche.expected
+++ b/tests/expected/valid-value-checks/custom_niche.expected
@@ -1,28 +1,19 @@
- ** 1 of 19 failed\
 Failed Checks: Undefined Behavior: Invalid value of type `Rating`
 
- ** 1 of 33 failed (4 unreachable)\
 Failed Checks: Kani currently doesn't support checking validity of `copy_nonoverlapping` for `*const Rating`
 
- ** 1 of 45 failed (4 unreachable)\
 Failed Checks: Kani currently doesn't support checking validity of `copy_nonoverlapping` for `*const Rating`
 
- ** 1 of 33 failed (4 unreachable)\
 Failed Checks: Undefined Behavior: Invalid value of type `Rating`
 
- ** 1 of 3 failed\
 Failed Checks: Undefined Behavior: Invalid value of type `Rating`
 
- ** 1 of 15 failed\
 Failed Checks: Undefined Behavior: Invalid value of type `Rating`
 
- ** 1 of 16 failed\
 Failed Checks: Undefined Behavior: Invalid value of type `Rating`
 
- ** 1 of 4 failed\
 Failed Checks: Undefined Behavior: Invalid value of type `Rating`
 
- ** 1 of 36 failed (1 unreachable)\
 Failed Checks: Undefined Behavior: Invalid value of type `Rating`
 
 Verification failed for - check_invalid_increment
diff --git a/tests/expected/valid-value-checks/non_null.expected b/tests/expected/valid-value-checks/non_null.expected
index 110fbf20a4c8..bc8572b879c6 100644
--- a/tests/expected/valid-value-checks/non_null.expected
+++ b/tests/expected/valid-value-checks/non_null.expected
@@ -1,7 +1,5 @@
- ** 1 of 39 failed (1 unreachable)\
 Failed Checks: Undefined Behavior: Invalid value of type `std::ptr::NonNull<u8>`
 
- ** 1 of 6 failed\
 Failed Checks: Undefined Behavior: Invalid value of type `std::ptr::NonNull<u8>`
 
 Verification failed for - check_invalid_value_cfg

From 9c12d793a7d6c26cf70747e2803b4a58ef0226a9 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 18 Feb 2025 10:33:47 +0000
Subject: [PATCH 10/10] Add failure description

---
 tests/expected/issue-3571/issue_3571.expected | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/tests/expected/issue-3571/issue_3571.expected b/tests/expected/issue-3571/issue_3571.expected
index 84191346398c..bed39a66b7af 100644
--- a/tests/expected/issue-3571/issue_3571.expected
+++ b/tests/expected/issue-3571/issue_3571.expected
@@ -1,2 +1,9 @@
+Failed Checks: misaligned pointer dereference: address must be a multiple of its type's alignment
+
+Failed Checks: null pointer dereference occurred
+
 VERIFICATION:- FAILED (encountered failures other than panics, which were unexpected)
+
+Verification failed for - rust_ub_should_fail
+Verification failed for - rust_ub_fails
 Complete - 0 successfully verified harnesses, 2 failures, 2 total.