Attribute Macro kani::should_panic
#[should_panic]Expand description
Specifies that a proof harness is expected to panic.**
This attribute allows users to exercise negative verification.
It’s analogous to how
#[should_panic]
allows users to exercise negative testing
for Rust unit tests.
§Limitations
The #[kani::should_panic] attribute verifies that there are one or more failed checks related to panics.
At the moment, it’s not possible to pin it down to specific panics.