From ccc1479f7863a126d5d3d6be877196181b5ff733 Mon Sep 17 00:00:00 2001
From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>
Date: Mon, 25 Apr 2022 12:16:49 -0400
Subject: [PATCH] Remove implementation for the `unreachable` intrinsic (#1100)

* Remove `unreachable` from intrinsics

* Add test for uses of `unreachable`
---
 .../src/codegen_cprover_gotoc/codegen/intrinsic.rs     |  6 ------
 tests/expected/intrinsics/unreachable/expected         |  2 ++
 tests/expected/intrinsics/unreachable/main.rs          | 10 ++++++++++
 3 files changed, 12 insertions(+), 6 deletions(-)
 create mode 100644 tests/expected/intrinsics/unreachable/expected
 create mode 100644 tests/expected/intrinsics/unreachable/main.rs

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
index 35a5217aaede..3b9dbe965838 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
@@ -607,12 +607,6 @@ impl<'tcx> GotocCtx<'tcx> {
             }
             "unchecked_sub" => codegen_op_with_overflow_check!(sub_overflow),
             "unlikely" => self.codegen_expr_to_place(p, fargs.remove(0)),
-            "unreachable" => self.codegen_assert(
-                Expr::bool_false(),
-                PropertyClass::DefaultAssertion,
-                "unreachable",
-                loc,
-            ),
             "volatile_copy_memory" => unstable_codegen!(codegen_intrinsic_copy!(Memmove)),
             "volatile_copy_nonoverlapping_memory" => {
                 unstable_codegen!(codegen_intrinsic_copy!(Memcpy))
diff --git a/tests/expected/intrinsics/unreachable/expected b/tests/expected/intrinsics/unreachable/expected
new file mode 100644
index 000000000000..a0b377e8e2e1
--- /dev/null
+++ b/tests/expected/intrinsics/unreachable/expected
@@ -0,0 +1,2 @@
+FAILURE\
+"unreachable code"
\ No newline at end of file
diff --git a/tests/expected/intrinsics/unreachable/main.rs b/tests/expected/intrinsics/unreachable/main.rs
new file mode 100644
index 000000000000..dab3f0b894bd
--- /dev/null
+++ b/tests/expected/intrinsics/unreachable/main.rs
@@ -0,0 +1,10 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+#![feature(core_intrinsics)]
+
+#[kani::proof]
+fn main() {
+    unsafe {
+        std::intrinsics::unreachable();
+    }
+}