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