Fix unreachable!() override macro + new tests (rust-lang#1372)

My latest change to handling panic messages actually broke `unreachable`
macro. The main issue was the wrong position of a parenthesis and the
fact that we didn't have tests that covered that specific case of the
macro.

One thing I haven't figured out yet is how to trigger an error if the
user code uses edition 2021+ and has the following construct:

```rust
let msg = "blah";
panic!(msg);
```

This is actually an error in 2021+, but the macro override that we
perform accepts that no matter the edition.

library/std/src/lib.rs

@@ -140,25 +140,54 @@ macro_rules! eprintln {
 
 #[macro_export]
 macro_rules! unreachable {
+    // The argument, if present, is a literal that represents the error message, i.e.:
+    // `unreachable!("Error message")` or `unreachable!()`
     ($($msg:literal)? $(,)?) => (
         kani::panic(concat!("internal error: entered unreachable code: ", $($msg)?))
     );
-    ($fmt:expr, $($arg:tt)*) => (
-        kani::panic(concat!("internal error: entered unreachable code: ", $fmt), stringify!($($arg)*)));
+    // The argument is an expression, such as a variable.
+    // ```
+    // let msg = format!("Error: {}", code);
+    // unreachable!(msg);
+    // ```
+    // This was supported for 2018 and older rust editions.
+    // TODO: Is it possible to trigger an error if 2021 and above?
+    // https://github.com/model-checking/kani/issues/1375
+    ($($msg:expr)? $(,)?) => (
+        kani::panic(concat!("internal error: entered unreachable code: ", stringify!($($msg)?)))
+    );
+    // The first argument is the format and the rest contains tokens to be included in the msg.
+    // `unreachable!("Error: {}", code);`
+    ($fmt:literal, $($arg:tt)*) => (
+        kani::panic(concat!("internal error: entered unreachable code: ",
+        stringify!($fmt, $($arg)*))));
 }
 
 #[macro_export]
 macro_rules! panic {
+    // No argument is given.
     () => (
         kani::panic("explicit panic")
     );
+    // The argument is a literal that represents the error message, i.e.:
+    // `panic!("Error message")`
     ($msg:literal $(,)?) => ({
         kani::panic(concat!($msg));
     });
+    // The argument is an expression, such as a variable.
+    // ```
+    // let msg = format!("Error: {}", code);
+    // panic!(msg);
+    // ```
+    // This was supported for 2018 and older rust editions.
+    // TODO: Is it possible to trigger an error if 2021 and above?
+    // https://github.com/model-checking/kani/issues/1375
     ($msg:expr $(,)?) => ({
         kani::panic(stringify!($msg));
     });
-    ($msg:expr, $($arg:tt)*) => ({
-        kani::panic(stringify!($msg, $($arg)*));
+    // The first argument is the format and the rest contains tokens to be included in the msg.
+    // `panic!("Error: {}", code);`
+    ($msg:literal, $($arg:tt)+) => ({
+        kani::panic(stringify!($msg, $($arg)+));
     });
 }

tests/expected/unreachable/expected

@@ -0,0 +1,6 @@
+Failed Checks: internal error: entered unreachable code: msg
+Failed Checks: internal error: entered unreachable code:
+Failed Checks: internal error: entered unreachable code: Error message
+Failed Checks: internal error: entered unreachable code: "Unreachable message with arg {}", "str"
+Failed Checks: internal error: entered unreachable code: "{}", msg
+

tests/expected/unreachable/unreach_msg.rs

@@ -0,0 +1,15 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Checks that our macro override supports different types of messages.
+#[kani::proof]
+fn check_unreachable() {
+    let msg = "Oops.";
+    match kani::any::<u8>() {
+        0 => unreachable!(),
+        1 => unreachable!("Error message"),
+        2 => unreachable!("Unreachable message with arg {}", "str"),
+        3 => unreachable!("{}", msg),
+        _ => unreachable!(msg),
+    }
+}