Stub panics during MIR transformation

tests/script-based-pre/mir_stub_panic/config.yml

@@ -0,0 +1,5 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: run.sh
+expected: expected
+exit_code: 0

tests/script-based-pre/mir_stub_panic/expected

@@ -0,0 +1,52 @@
+--VERIFYING panic.rs--
+Manual Harness Summary: \
+Verification failed for - main \
+Complete - 0 successfully verified harnesses, 1 failures, 1 total.
+
+--READING MIR for panic.rs--
+fn kani::rustc_intrinsics::panic_stub(_1: &str) -> ! { \
+    let mut _0: !; \
+    debug t => _1; \
+    bb0: { \
+        goto -> bb1; \
+    } \
+    bb1: { \
+        goto -> bb1; \
+    } \
+}
+
+
+--VERIFYING option.rs--
+Manual Harness Summary: \
+Verification failed for - main \
+Complete - 0 successfully verified harnesses, 1 failures, 1 total.
+
+--READING MIR for option.rs--
+fn kani::rustc_intrinsics::panic_stub(_1: &str) -> ! { \
+    let mut _0: !; \
+    debug t => _1; \
+    bb0: { \
+        goto -> bb1; \
+    } \
+    bb1: { \
+        goto -> bb1; \
+    } \
+}
+
+
+--VERIFYING result.rs--
+Manual Harness Summary: \
+Verification failed for - main \
+Complete - 0 successfully verified harnesses, 1 failures, 1 total.
+
+--READING MIR for result.rs--
+fn kani::rustc_intrinsics::panic_stub(_1: &str) -> ! { \
+    let mut _0: !; \
+    debug t => _1; \
+    bb0: { \
+        goto -> bb1; \
+    } \
+    bb1: { \
+        goto -> bb1; \
+    } \
+}

tests/script-based-pre/mir_stub_panic/option.rs

@@ -0,0 +1,13 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Ensure the panic!() internal to `Option::unwrap()` is stubbed.
+#[kani::proof]
+fn main() {
+    foo();
+}
+
+fn foo() -> usize {
+    let a: Option<usize> = kani::any();
+    a.unwrap()
+}

tests/script-based-pre/mir_stub_panic/panic.rs

@@ -0,0 +1,8 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Ensure that the panic!() macro itself gets stubbed.
+#[kani::proof]
+fn main() {
+    panic!("hello!");
+}

tests/script-based-pre/mir_stub_panic/result.rs

@@ -0,0 +1,13 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Ensure the panic!() internal to `Result::unwrap()` is stubbed.
+#[kani::proof]
+fn main() {
+    foo();
+}
+
+fn foo() -> usize {
+    let a: Result<usize, usize> = kani::any();
+    a.unwrap()
+}

tests/script-based-pre/mir_stub_panic/run.sh

@@ -0,0 +1,17 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+echo "--VERIFYING panic.rs--"
+RUSTFLAGS="--emit mir" kani panic.rs
+echo "--READING MIR for panic.rs--"
+cat panic__*
+
+echo "--VERIFYING option.rs--"
+RUSTFLAGS="--emit mir" kani option.rs
+echo "--READING MIR for option.rs--"
+cat option__*
+
+echo "--VERIFYING result.rs--"
+RUSTFLAGS="--emit mir" kani result.rs
+echo "--READING MIR for result.rs--"
+cat result__*