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.

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?

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:

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.

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

Closing as no longer needed.