Turn off debug assertions under --prove-safety-only

kani-driver/src/call_single_file.rs

@@ -228,6 +228,11 @@ impl KaniSession {
             flags.push("-Zmir-enable-passes=-SingleUseConsts".into());
         }
 
+        if self.args.prove_safety_only {
+            flags.push("-C".into());
+            flags.push("debug-assertions=off".into());
+        }
+
         // This argument will select the Kani flavour of the compiler. It will be removed before
         // rustc driver is invoked.
         flags.push("--kani-compiler".into());

library/std/src/lib.rs

@@ -124,19 +124,19 @@ macro_rules! assert_ne {
 #[cfg(not(feature = "concrete_playback"))]
 #[macro_export]
 macro_rules! debug_assert {
-    ($($x:tt)*) => ({ $crate::assert!($($x)*); })
+    ($($x:tt)*) => ({ if cfg!(debug_assertions) { $crate::assert!($($x)*); } })
 }
 
 #[cfg(not(feature = "concrete_playback"))]
 #[macro_export]
 macro_rules! debug_assert_eq {
-    ($($x:tt)*) => ({ $crate::assert_eq!($($x)*); })
+    ($($x:tt)*) => ({ if cfg!(debug_assertions) { $crate::assert_eq!($($x)*); } })
 }
 
 #[cfg(not(feature = "concrete_playback"))]
 #[macro_export]
 macro_rules! debug_assert_ne {
-    ($($x:tt)*) => ({ $crate::assert_ne!($($x)*); })
+    ($($x:tt)*) => ({ if cfg!(debug_assertions) { $crate::assert_ne!($($x)*); } })
 }
 
 // Override the print macros to skip all the printing functionality (which

tests/expected/safety-debug_assert/prove_safety_only.expected

@@ -0,0 +1,14 @@
+<usize as kani::rustc_intrinsics::ToISize>::to_isize.safety_check\
+	 - Status: FAILURE\
+	 - Description: "Offset value overflows isize"
+
+kani::rustc_intrinsics::offset::<u8, *const u8, usize>.safety_check\
+	 - Status: FAILURE\
+	 - Description: "Offset result and original pointer must point to the same allocation"
+
+Failed Checks: Offset value overflows isize
+Failed Checks: Offset result and original pointer must point to the same allocation
+
+VERIFICATION:- FAILED
+Verification failed for - debug_assert_does_not_hide_ub
+Complete - 0 successfully verified harnesses, 1 failures, 1 total.

tests/expected/safety-debug_assert/prove_safety_only.rs

@@ -0,0 +1,15 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// kani-flags: -Z unstable-options --prove-safety-only
+//! Test that --prove-safety-only turns debug_assert into a no-op
+
+#[kani::proof]
+fn debug_assert_does_not_hide_ub() {
+    let arr: [u8; 5] = kani::any();
+    let bytes = kani::slice::any_slice_of_array(&arr);
+    let slice_offset = unsafe { bytes.as_ptr().offset_from(&arr as *const u8) };
+    let offset: usize = kani::any();
+    debug_assert!(offset <= 4 && (slice_offset as usize) + offset <= 4);
+    let _ = unsafe { *bytes.as_ptr().add(offset) };
+}