Ignore messages for assert, panic, and unreachable macros

library/std/src/lib.rs

@@ -41,21 +41,14 @@ macro_rules! assert {
         kani::assert($cond, concat!("assertion failed: ", stringify!($cond)));
     };
     ($cond:expr, $($arg:tt)+) => {{
+        // Note that by stringifying the arguments to the custom message, any
+        // compile-time checks on those arguments (e.g. checking that a symbol
+        // is defined and that it implements the Display trait) are bypassed:
+        // https://github.com/model-checking/kani/issues/803
+        // In addition, Kani may emit spurious compiler warnings due to unused
+        // variables:
+        // https://github.com/model-checking/kani/issues/1556
         kani::assert($cond, concat!(stringify!($($arg)+)));
-        // Process the arguments of the assert inside an unreachable block. This
-        // is to make sure errors in the arguments (e.g. an unknown variable or
-        // an argument that does not implement the Display or Debug traits) are
-        // reported, without creating any overhead on verification performance
-        // that may arise from processing strings involved in the arguments.
-        // Note that this approach is only correct with the "abort" panic
-        // strategy, but is unsound with the "unwind" panic strategy which
-        // requires evaluating the arguments (because they might have side
-        // effects). This is fine until we add support for the "unwind" panic
-        // strategy, which is tracked in
-        // https://github.com/model-checking/kani/issues/692
-        if false {
-            ::std::panic!($($arg)+);
-        }
     }};
 }
 
@@ -157,9 +150,6 @@ macro_rules! unreachable {
     // We have the same issue as with panic!() described bellow where we over-approx what we can
     // handle.
     ($fmt:expr, $($arg:tt)*) => {{
-        if false {
-            let _ = format_args!($fmt, $($arg)+);
-        }
         kani::panic(concat!("internal error: entered unreachable code: ",
         stringify!($fmt, $($arg)*)))}};
 }
@@ -199,9 +189,6 @@ macro_rules! panic {
     // be able to do things that we cannot do here.
     // https://github.com/rust-lang/rust/blob/dc2d232c7485c60dd856f8b9aee83426492d4661/compiler/rustc_expand/src/base.rs#L1197
     ($msg:expr, $($arg:tt)+) => {{
-        if false {
-            let _ = format_args!($msg, $($arg)+);
-        }
         kani::panic(stringify!($msg, $($arg)+));
     }};
 }

tests/expected/panic/const-fn/expected

@@ -0,0 +1 @@
+Failed Checks: "{}", msg

tests/expected/panic/const-fn/test.rs

@@ -0,0 +1,16 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test checks that `panic!` with args can be used in a const fn
+
+const fn my_const_fn(msg: &str) -> ! {
+    panic!("{}", msg)
+}
+
+#[kani::proof]
+pub fn check_something() {
+    let x = 5;
+    if x > 2 {
+        my_const_fn("function will panic");
+    }
+}

tests/kani/Assert/var_in_arg.rs → tests/kani/Assert/var_in_arg_fixme.rs

@@ -3,6 +3,8 @@
 
 //! This test makes sure Kani does not emit "unused variable" warnings for
 //! variables that are only used in arguments of assert macros
+//! This doesn't work currently:
+//! https://github.com/model-checking/kani/issues/1556
 
 // Promote "unused variable" warnings to an error so that this test fails if
 // Kani's overridden version of the assert macros drops variables used as

tests/kani/Panic/compile_panic.rs

@@ -0,0 +1,15 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-check-fail
+
+//! This test checks that Kani fails in compilation due to a panic evaluated at
+//! compile time
+
+const fn my_const_fn(x: i32) -> i32 {
+    if x > 0 { x - 1 } else { panic!("x is negative") }
+}
+
+#[kani::proof]
+pub fn check_something() {
+    const _X: i32 = my_const_fn(-3);
+}

tests/kani/StdOverrides/arg.rs → tests/kani/StdOverrides/arg_fixme.rs

@@ -3,6 +3,8 @@
 
 //! This test makes sure Kani does not emit "unused variable" warnings for
 //! variables that are only used in arguments of panic/unreachable macros
+//! This doesn't work currently:
+//! https://github.com/model-checking/kani/issues/1556
 
 // Promote "unused variable" warnings to an error so that this test fails if
 // Kani's overridden version of the panic/unreachable macros drops variables