Attribute Macro vstd::prelude::invariant_except_break

#[invariant_except_break]