vstd_extra/panic.rs
1//! Runtime panic helper whose type (`-> !`) lets Verus discharge
2//! post-conditions by branch elimination at the call site.
3use vstd::prelude::*;
4use vstd::vpanic;
5
6verus! {
7
8/// Unconditionally diverges. Callers use `if bad { panic_diverge(); }` as a
9/// runtime check that Verus accepts as establishing `!bad` afterwards.
10#[verifier::external_body]
11pub fn panic_diverge() -> ! {
12 vpanic!("panic_diverge")
13}
14
15} // verus!