From 6a8e33f0336a664727410d5617312b3290564815 Mon Sep 17 00:00:00 2001
From: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
Date: Fri, 26 Aug 2022 10:45:53 -0700
Subject: [PATCH] Make panic and assert const functions (#1590)

---
 library/kani/src/lib.rs          |  4 ++--
 tests/kani/Assert/in_const_fn.rs | 15 +++++++++++++++
 tests/kani/Panic/const.rs        | 16 ++++++++++++++++
 3 files changed, 33 insertions(+), 2 deletions(-)
 create mode 100644 tests/kani/Assert/in_const_fn.rs
 create mode 100644 tests/kani/Panic/const.rs

diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs
index 151a4f220e27..e4b456431cc0 100644
--- a/library/kani/src/lib.rs
+++ b/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)
 }
 
diff --git a/tests/kani/Assert/in_const_fn.rs b/tests/kani/Assert/in_const_fn.rs
new file mode 100644
index 000000000000..064a3f869b37
--- /dev/null
+++ b/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);
+}
diff --git a/tests/kani/Panic/const.rs b/tests/kani/Panic/const.rs
new file mode 100644
index 000000000000..ddffa53d5517
--- /dev/null
+++ b/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();
+    }
+}