Remove implementation for the unreachable intrinsic (#1100)

* Remove `unreachable` from intrinsics

* Add test for uses of `unreachable`

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))

tests/expected/intrinsics/unreachable/expected

@@ -0,0 +1,2 @@
+FAILURE\
+"unreachable code"

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();
+    }
+}