// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT

// See discussion on https://github.com/model-checking/kani/issues/267
#![feature(core_intrinsics)]
use std::intrinsics::r#try;

#[kani::proof]
fn main() {
    unsafe {
        // Rust will make a best-effort to swallow the panic, and then execute the cleanup function.
        // However, my understanding is that failure is still possible, since its just a best-effort
        r#try(
            |_a: *mut u8| panic!("foo"),
            std::ptr::null_mut(),
            |_a: *mut u8, _b: *mut u8| println!("bar"),
        );
    }
}