// Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // This example is a copy of the `cbmc` test in // `src/test/kani/LoopLoop_NonReturning/main_no_unwind_asserts.rs` // // The verification output should show an unwinding assertion failure. // // In this test, we check that Kani warns the user about unwinding failures // and makes a recommendation to fix the issue. #[kani::proof] #[kani::unwind(9)] fn main() { let mut a: u32 = kani::any(); if a < 1024 { loop { a = a / 2; if a == 0 { break; } } assert!(a == 0); } }