Skip to main content

panic_diverge

vstd_extra::panic

Function panic_diverge 

Source 
pub exec fn panic_diverge() -> !
Expand description

Unconditionally diverges. Callers use if bad { panic_diverge(); } as a runtime check that Verus accepts as establishing !bad afterwards.