Prefix property descriptions of panics with "Panic:"

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"

tests/cargo-kani/codegen-scalar-with-phantom/check_phantom_data.expected

@@ -1,4 +1,4 @@
 Status: SUCCESS\
-Description: "assertion failed: C.x == 0"
+Description: "Panic: assertion failed: C.x == 0"
 
 VERIFICATION:- SUCCESSFUL

tests/cargo-kani/codegen-scalar-with-zsts/check_zst.expected

@@ -1,4 +1,4 @@
 Status: SUCCESS\
-Description: "assertion failed: C.x == 0"
+Description: "Panic: assertion failed: C.x == 0"
 
 VERIFICATION:- SUCCESSFUL

tests/cargo-kani/demos/non-empty-range/check_range.expected

@@ -1,4 +1,4 @@
 Status: SUCCESS\
-Description: "assertion failed: range.is_none() || !range.as_ref().unwrap().is_empty()"
+Description: "Panic: assertion failed: range.is_none() || !range.as_ref().unwrap().is_empty()"
 
 VERIFICATION:- SUCCESSFUL

tests/cargo-kani/itoa_dep/check_unsigned.expected

@@ -1,4 +1,4 @@
 Status: SUCCESS\
-Description: "assertion failed: result == &output"
+Description: "Panic: assertion failed: result == &output"
 
 VERIFICATION:- SUCCESSFUL

tests/cargo-kani/nested-dirs/crate1/a_check.expected

@@ -1,3 +1,3 @@
 Status: SUCCESS\
-Description: "assertion failed: v.len() == 3"
+Description: "Panic: assertion failed: v.len() == 3"
 VERIFICATION:- SUCCESSFUL

tests/cargo-kani/nested-dirs/crate2/another_check.expected

@@ -1,3 +1,3 @@
 Status: SUCCESS\
-Description: "assertion failed: result == 4"
+Description: "Panic: assertion failed: result == 4"
 VERIFICATION:- SUCCESSFUL

tests/cargo-kani/nested-dirs/crate2/nested_crate/yet_another_check.expected

@@ -1,4 +1,4 @@
 Status: SUCCESS\
-Description: "assertion failed: y - x == 0"
+Description: "Panic: assertion failed: y - x == 0"
 
 VERIFICATION:- SUCCESSFUL

tests/cargo-kani/output-format/main.expected

@@ -1 +1 @@
-Description: "assertion failed: 1 + 1 == 2"
+Description: "Panic: assertion failed: 1 + 1 == 2"

tests/cargo-kani/small-vec/check_vec.expected

@@ -1,5 +1,5 @@
 Status: SUCCESS\
-Description: "assertion failed: c < char::MAX"\
+Description: "Panic: assertion failed: c < char::MAX"\
 in function check_vec
 
 VERIFICATION:- SUCCESSFUL

tests/cargo-kani/stubbing-ws-packages/expected

@@ -1,25 +1,25 @@
 Checking harness verify::check_no_stub...
 Status: SUCCESS\
-Description: "assertion failed: config == StubConfig::NoStub"
+Description: "Panic: assertion failed: config == StubConfig::NoStub"
 VERIFICATION:- SUCCESSFUL
 
 Checking harness verify::check_stub_1...
 Status: SUCCESS\
-Description: "assertion failed: config == StubConfig::Stub1"
+Description: "Panic: assertion failed: config == StubConfig::Stub1"
 VERIFICATION:- SUCCESSFUL
 
 Checking harness verify_top::check_no_stub...
 Status: SUCCESS\
-Description: "assertion failed: stub_id() == None"
+Description: "Panic: assertion failed: stub_id() == None"
 VERIFICATION:- SUCCESSFUL
 
 Checking harness verify_top::check_stub_1...
 Status: SUCCESS\
-Description: "assertion failed: stub_id() == Some(1)"
+Description: "Panic: assertion failed: stub_id() == Some(1)"
 VERIFICATION:- SUCCESSFUL
 
 Checking harness verify_top::check_stub_2...
 Status: SUCCESS\
-Description: "assertion failed: stub_id() == Some(2)"
+Description: "Panic: assertion failed: stub_id() == Some(2)"
 
 Complete - 5 successfully verified harnesses, 0 failures, 5 total.

tests/cargo-kani/vecdeque-cve/reserve_available_capacity_is_no_op.expected

@@ -1,17 +1,17 @@
 fixed::VecDeque::<u8>::handle_capacity_increase.assertion\
 Status: UNREACHABLE\
-Description: "assertion failed: self.head < self.tail"
+Description: "Panic: assertion failed: self.head < self.tail"
 
 fixed::VecDeque::<u8>::handle_capacity_increase.assertion\
 Status: UNREACHABLE\
-Description: "assertion failed: self.head < self.cap()"
+Description: "Panic: assertion failed: self.head < self.cap()"
 
 fixed::VecDeque::<u8>::handle_capacity_increase.assertion\
 Status: UNREACHABLE\
-Description: "assertion failed: self.tail < self.cap()"
+Description: "Panic: assertion failed: self.tail < self.cap()"
 
 fixed::VecDeque::<u8>::handle_capacity_increase.assertion\
 Status: UNREACHABLE\
-Description: "assertion failed: self.cap().count_ones() == 1"
+Description: "Panic: assertion failed: self.cap().count_ones() == 1"
 
 VERIFICATION:- SUCCESSFUL

tests/cargo-kani/vecdeque-cve/reserve_available_capacity_should_fail.expected

@@ -1,6 +1,6 @@
 cve::VecDeque::<u8>::handle_capacity_increase.assertion\
 - Status: FAILURE\
-- Description: "assertion failed: self.head < self.cap()"
+- Description: "Panic: assertion failed: self.head < self.cap()"
 Location: src/cve.rs
 
-Failed Checks: assertion failed: self.head < self.cap()
+Failed Checks: Panic: assertion failed: self.head < self.cap()

tests/cargo-kani/vecdeque-cve/reserve_more_capacity_still_works.expected

@@ -1,16 +1,16 @@
 cve::VecDeque::<u8>::handle_capacity_increase.assertion\
 Status: SUCCESS\
-Description: "assertion failed: self.head < self.cap()"\
+Description: "Panic: assertion failed: self.head < self.cap()"\
 Location: src/cve.rs
 
 cve::VecDeque::<u8>::handle_capacity_increase.assertion\
 Status: SUCCESS\
-Description: "assertion failed: self.tail < self.cap()"\
+Description: "Panic: assertion failed: self.tail < self.cap()"\
 Location: src/cve.rs
 
 cve::VecDeque::<u8>::handle_capacity_increase.assertion\
 Status: SUCCESS\
-Description: "assertion failed: self.cap().count_ones() == 1"\
+Description: "Panic: assertion failed: self.cap().count_ones() == 1"\
 Location: src/cve.rs
 
 VERIFICATION:- SUCCESSFUL

tests/cargo-kani/vecdeque-cve/reserve_more_capacity_works.expected

@@ -1,16 +1,16 @@
 fixed::VecDeque::<u8>::handle_capacity_increase.assertion\
 Status: SUCCESS\
-Description: "assertion failed: self.head < self.cap()"\
+Description: "Panic: assertion failed: self.head < self.cap()"\
 Location: src/fixed.rs
 
 fixed::VecDeque::<u8>::handle_capacity_increase.assertion\
 Status: SUCCESS\
-Description: "assertion failed: self.tail < self.cap()"\
+Description: "Panic: assertion failed: self.tail < self.cap()"\
 Location: src/fixed.rs
 
 fixed::VecDeque::<u8>::handle_capacity_increase.assertion\
 Status: SUCCESS\
-Description: "assertion failed: self.cap().count_ones() == 1"\
+Description: "Panic: assertion failed: self.cap().count_ones() == 1"\
 Location: src/fixed.rs
 
 VERIFICATION:- SUCCESSFUL

tests/expected/abort/expected

@@ -1,5 +1,5 @@
 Status: UNREACHABLE\
-Description: ""This is unreachable""\
+Description: "Panic: "This is unreachable""\
 in function main
 
 Status: FAILURE\

tests/expected/arbitrary/duration.expected

@@ -19,7 +19,7 @@ Status: SATISFIED\
 Description: "Max nanos"
 
 Status: SUCCESS\
-Description: ""Is Zero""
+Description: "Panic: "Is Zero""
 
 6 of 6 cover properties satisfied
 1 successfully verified harnesses, 0 failures

tests/expected/arbitrary/ptrs/pointer_generator.expected

@@ -1,21 +1,21 @@
 Checking harness check_arbitrary_ptr...
 
 Status: SUCCESS\
-Description: ""OutOfBounds""
+Description: "Panic: "OutOfBounds""
 
 Status: SUCCESS\
-Description: ""InBounds""
+Description: "Panic: "InBounds""
 
 Status: SUCCESS\
-Description: ""NullPtr""
+Description: "Panic: "NullPtr""
 
 Status: FAILURE\
-Description: ""DeadObject""
+Description: "Panic: "DeadObject""
 
 Status: SATISFIED\
 Description: "Dangling"
 
 Status: UNREACHABLE\
-Description: ""Dangling write""
+Description: "Panic: "Dangling write""
 
 Verification failed for - check_arbitrary_ptr

tests/expected/arbitrary/ptrs/pointer_inbounds.expected

@@ -15,15 +15,15 @@ Description: "Smaller"
 Checking harness check_alignment...
 
 Status: SUCCESS\
-Description: ""Aligned""
+Description: "Panic: "Aligned""
 
 Status: SUCCESS\
-Description: ""Unaligned""
+Description: "Panic: "Unaligned""
 
 Checking harness check_inbounds_initialized...
 
 Status: SUCCESS\
-Description: ""ValidRead""
+Description: "Panic: "ValidRead""
 
 Checking harness check_inbounds...
 
@@ -34,6 +34,6 @@ Status: SATISFIED\
 Description: "Initialized"
 
 Status: SUCCESS\
-Description: ""ValidWrite""
+Description: "Panic: "ValidWrite""
 
 Complete - 4 successfully verified harnesses, 0 failures, 4 total.

tests/expected/arith_checks/expected

@@ -1 +1 @@
-Failed Checks: attempt to subtract with overflow
+Failed Checks: Panic: attempt to subtract with overflow

tests/expected/assert-eq-chained/expected

@@ -1,13 +1,13 @@
 Status: SUCCESS\
-Description: "assertion failed: x > 3 == true"
+Description: "Panic: assertion failed: x > 3 == true"
 
 Status: SUCCESS\
-Description: "assertion failed: x == 1 == false"
+Description: "Panic: assertion failed: x == 1 == false"
 
 Status: SUCCESS\
-Description: "assertion failed: x < 10 != false"
+Description: "Panic: assertion failed: x < 10 != false"
 
 Status: FAILURE\
-Description: "assertion failed: x == 7 != false"
+Description: "Panic: assertion failed: x == 7 != false"
 
 VERIFICATION:- FAILED

tests/expected/assert-location/assert-false/expected

@@ -1,3 +1,3 @@
-line 18 assertion failed: false: FAILURE
-line 23 "{}", s: FAILURE
-line 27 "Fail with custom static message": FAILURE
+line 18 Panic: assertion failed: false: FAILURE
+line 23 Panic: "{}", s: FAILURE
+line 27 Panic: "Fail with custom static message": FAILURE

tests/expected/assert-location/debug-assert/expected

@@ -1,2 +1,2 @@
-line 13 "This should fail and stop the execution": FAILURE
-line 14 "This should be unreachable": SUCCESS
+line 13 Panic: "This should fail and stop the execution": FAILURE
+line 14 Panic: "This should be unreachable": SUCCESS

tests/expected/coroutines/expected

@@ -1,10 +1,10 @@
 SUCCESS\
-Description: "assertion failed: res == CoroutineState::Yielded(val)"
+Description: "Panic: assertion failed: res == CoroutineState::Yielded(val)"
 
 SUCCESS\
-Description: "assertion failed: res == CoroutineState::Complete(!val)"
+Description: "Panic: assertion failed: res == CoroutineState::Complete(!val)"
 
 UNREACHABLE\
-Description: "coroutine resumed after completion"
+Description: "Panic: coroutine resumed after completion"
 
 VERIFICATION:- SUCCESSFUL

tests/expected/coroutines/pin/expected

@@ -7,7 +7,7 @@ Description: "unexpected yield from resume"\
 in function main
 
 UNREACHABLE\
-Description: "coroutine resumed after completion"
+Description: "Panic: coroutine resumed after completion"
 in function main::{closure#0}
 
 VERIFICATION:- SUCCESSFUL