Make panic and assert const functions (#1590)

library/kani/src/lib.rs

@@ -58,7 +58,7 @@ pub fn assume(_cond: bool) {
 /// ```
 #[inline(never)]
 #[rustc_diagnostic_item = "KaniAssert"]
-pub fn assert(_cond: bool, _msg: &'static str) {
+pub const fn assert(_cond: bool, _msg: &'static str) {
     if cfg!(feature = "concrete_playback") {
         assert!(_cond, "{}", _msg);
     }
@@ -134,7 +134,7 @@ pub fn expect_fail(_cond: bool, _message: &'static str) {
 #[inline(never)]
 #[rustc_diagnostic_item = "KaniPanic"]
 #[doc(hidden)]
-pub fn panic(message: &'static str) -> ! {
+pub const fn panic(message: &'static str) -> ! {
     panic!("{}", message)
 }
 

tests/kani/Assert/in_const_fn.rs

@@ -0,0 +1,15 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test checks that `assert!` can be used in a const fn
+
+const fn const_add(x: i32, y: i32) {
+    assert!(x + y == x);
+}
+
+#[kani::proof]
+fn check() {
+    let x = kani::any();
+    let y = 0;
+    const_add(x, y);
+}

tests/kani/Panic/const.rs

@@ -0,0 +1,16 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test checks that `panic!` can be used in a const fn
+
+const fn my_const_fn() {
+    panic!()
+}
+
+#[kani::proof]
+pub fn check_something() {
+    let x: u8 = if kani::any() { 3 } else { 95 };
+    if x > 100 {
+        my_const_fn();
+    }
+}