Prefix property descriptions of panics with "Panic:"

This will reduce the ambiguity between cases of Kani reporting a safety
(undefined behavior) violation vs Kani demonstrating the possibility of
a panic (defined behavior).

Author: tautschnig

docs/src/getting-started/verification-results/failure_example.expected

@@ -1,2 +1,2 @@
 FAILURE\
-Description: "assertion failed: arr.len() != 3"
+Description: "Panic: assertion failed: arr.len() != 3"

docs/src/getting-started/verification-results/success_example.expected

@@ -1,2 +1,2 @@
 SUCCESS\
-Description: "assertion failed: sum == 6"
+Description: "Panic: assertion failed: sum == 6"

docs/src/getting-started/verification-results/undetermined_example.expected

@@ -1,2 +1,2 @@
 UNDETERMINED\
-Description: "assertion failed: x == 0"
+Description: "Panic: assertion failed: x == 0"

docs/src/getting-started/verification-results/unreachable_example.expected

@@ -1,2 +1,2 @@
 UNREACHABLE\
-Description: "assertion failed: x < 8"
+Description: "Panic: assertion failed: x < 8"

kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs

@@ -231,7 +231,7 @@ impl GotocCtx<'_> {
         // If there is one in the MIR, use it; otherwise, explain that we can't.
         assert!(!fargs.is_empty(), "Panic requires a string message");
         let msg = self.extract_const_message(&fargs[0]).unwrap_or(String::from(
-            "This is a placeholder message; Kani doesn't support message formatted at runtime",
+            "Panic: This is a placeholder message; Kani doesn't support message formatted at runtime",
         ));
         self.codegen_fatal_error(PropertyClass::Assertion, &msg, span)
     }

kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs

@@ -261,7 +261,7 @@ impl GotocCtx<'_> {
                         // "index out of bounds: the length is {len} but the index is {index}",
                         // but CBMC only accepts static messages so we don't add values to the message.
                         (
-                            "index out of bounds: the length is less than or equal to the given index",
+                            "Panic: index out of bounds: the length is less than or equal to the given index".to_string(),
                             PropertyClass::Assertion,
                         )
                     }
@@ -270,22 +270,23 @@ impl GotocCtx<'_> {
                         // Generate a generic one here.
                         (
                             "misaligned pointer dereference: address must be a multiple of its type's \
-                    alignment",
+                    alignment".to_string(),
                             PropertyClass::SafetyCheck,
                         )
                     }
                     // For all other assert kind we can get the static message.
                     AssertMessage::NullPointerDereference => {
-                        (msg.description().unwrap(), PropertyClass::SafetyCheck)
+                        (msg.description().unwrap().to_string(), PropertyClass::SafetyCheck)
                     }
                     AssertMessage::Overflow { .. }
                     | AssertMessage::OverflowNeg { .. }
                     | AssertMessage::DivisionByZero { .. }
                     | AssertMessage::RemainderByZero { .. }
                     | AssertMessage::ResumedAfterReturn { .. }
-                    | AssertMessage::ResumedAfterPanic { .. } => {
-                        (msg.description().unwrap(), PropertyClass::Assertion)
-                    }
+                    | AssertMessage::ResumedAfterPanic { .. } => (
+                        "Panic: ".to_owned() + msg.description().unwrap(),
+                        PropertyClass::Assertion,
+                    ),
                 };
 
                 let (msg_str, reach_stmt) =

kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs

@@ -137,7 +137,12 @@ impl GotocHook for Assert {
         Stmt::block(
             vec![
                 reach_stmt,
-                gcx.codegen_assert_assume(cond, PropertyClass::Assertion, &msg, caller_loc),
+                gcx.codegen_assert_assume(
+                    cond,
+                    PropertyClass::Assertion,
+                    &("Panic: ".to_owned() + &msg),
+                    caller_loc,
+                ),
                 Stmt::goto(bb_label(target), caller_loc),
             ],
             caller_loc,
@@ -272,7 +277,12 @@ impl GotocHook for Check {
         Stmt::block(
             vec![
                 reach_stmt,
-                gcx.codegen_assert(cond, PropertyClass::Assertion, &msg, caller_loc),
+                gcx.codegen_assert(
+                    cond,
+                    PropertyClass::Assertion,
+                    &("Panic: ".to_owned() + &msg),
+                    caller_loc,
+                ),
                 Stmt::goto(bb_label(target), caller_loc),
             ],
             caller_loc,

tests/cargo-kani/asm/global/calls_crate_with_global_asm.expected

@@ -1,2 +1,2 @@
 Status: SUCCESS\
-Description: "assertion failed: x * y == 33"
+Description: "Panic: assertion failed: x * y == 33"

tests/cargo-kani/asm/global/reads_static_var_in_crate_with_global_asm.expected

@@ -1,2 +1,2 @@
 Status: SUCCESS\
-Description: "assertion failed: x == 98"
+Description: "Panic: assertion failed: x == 98"

tests/cargo-kani/assert-reach/test.expected

@@ -1,2 +1,2 @@
 UNREACHABLE\
-Description: "assertion failed: z == x - 1"
+Description: "Panic: assertion failed: z == x - 1"