Prefix property descriptions of panics with "Panic:"

[tautschnig]

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

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[zhassan-aws]

Is it not possible to rely on the property class for this disambiguation? We've been trying to avoid modifying assertion messages that come from the compiler.

[tautschnig]

Is it not possible to rely on the property class for this disambiguation? We've been trying to avoid modifying assertion messages that come from the compiler.

I guess that would require also printing the property class when reporting results?

[zhassan-aws]

I guess what I'm missing is the target audience of this change. Is it for human consumption? If not, Kani's CBMC property parser processes the property class:

kani/kani-driver/src/cbmc_output_parser.rs

Line 101 in 7209765

pub fn property_class(&self) -> String {

[tautschnig]

I guess what I'm missing is the target audience of this change.

My current reason for putting forth this change proposal is that we were reviewing results on the standard library and didn't know whether we were seeing reports of undefined behavior or possible panics.

[zhassan-aws]

My current reason for putting forth this change proposal is that we were reviewing results on the standard library and didn't know whether we were seeing reports of undefined behavior or possible panics.

And this cannot be inferred from the first line of a check's output? e.g.:

Check 94: std::ptr::write::<std::mem::MaybeUninit<usize>>.pointer_dereference.5
         - Status: SUCCESS
         - Description: "dereference failure: pointer outside object bounds"
         - Location: ../.rustup/toolchains/nightly-2025-01-28-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1582:9 in function std::ptr::write::<std::mem::MaybeUninit<usize>>

which shows that this is a pointer_dereference check.

(Sorry for asking too many questions. I just want to make sure this change is warranted.)