UB checks should fail verification for harnesses annotated with #[should_panic]
#3571
Labels
[C] Feature / Enhancement
A new feature request or enhancement to an existing feature.
[E] User Experience
An UX enhancement for an existing feature. Including deprecation of an existing one.
I believe we need to create a new UB check property category, and audit the compiler to use the new category for UB instrumentation. The
#[should_panic]
implementation should take this new category into consideration. Note that this is already the case for some UB's checks.The motivation is to allow users to write safety harness that succeed as long as no UB is detected.
Here is a small example of how Kani inconsistencyt:
Running this with kani:
The text was updated successfully, but these errors were encountered: