Add "fixme" testcase for rust-lang#1208 (rust-lang#1210)

* Add "fixme" testcase for rust-lang#1208

I also added an override for the `unreachable!()` macro to print nicer
error message.

* Document override + test

docs/src/overrides.md

@@ -18,3 +18,5 @@ Name | Description |
 `assert`, `assert_eq`, and `assert_ne` macros | Skips string formatting code, generates a more informative message and performs some instrumentation |
 `debug_assert`, `debug_assert_eq`, and `debug_assert_ne` macros | Rewrites as equivalent `assert*` macro |
 `print`, `eprint`, `println`, and `eprintln` macros | Skips string formatting and I/O operations |
+`unreachable` macro | Skips string formatting and invokes `panic!()` |
+`std::process::{abort, exit}` functions | Invokes `panic!()` to abort the execution |

library/std/src/lib.rs

@@ -137,3 +137,11 @@ macro_rules! println {
 macro_rules! eprintln {
     ($($x:tt)*) => { evaluate_print_args!($($x)*); };
 }
+
+#[macro_export]
+macro_rules! unreachable {
+    ($($arg:tt)*) => ({
+        panic!(concat!("internal error: entered unreachable code: ",
+        stringify!($($arg)*)));
+    });
+}

tests/expected/arith_checks/expected

@@ -0,0 +1,2 @@
+Failed Checks: attempt to subtract with overflow
+Failed Checks: internal error: entered unreachable code: "Previous statement should fail"

tests/expected/arith_checks/fixme_check_arith_failures.rs

@@ -0,0 +1,13 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Checks that code after an overflow check failure should be unreachable.
+//! Related issue: https://github.com/model-checking/kani/issues/1208
+#[kani::proof]
+fn check_arith_overflow() {
+    let a = [0; 5];
+    let ptr0: *const i32 = &a[0];
+    let ptr1: *const i32 = &a[1];
+    let _: usize = ptr0 as usize - ptr1 as usize;
+    unreachable!("Previous statement should fail");
+}