Function vstd::pervasive::allow_panic

source · 
pub open spec fn allow_panic() -> bool
Expand description
{ cfg!(feature = "allow_panic") }

The default behavior of the vstd library enforces writing panic-free code. While developers may still use panic, verification should ensure that any panic is provably unreachable. cfg!(feature = “allow_panic”) explicily allows code to panic.