forked from model-checking/kani
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
use codegen_unimplemented() for the try intrinsic (model-checking#275)
* use codegen_unimplemented() for the try intrinsic * Additional unit test
- Loading branch information
Showing
4 changed files
with
63 additions
and
9 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,18 @@ | ||
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. | ||
// SPDX-License-Identifier: Apache-2.0 OR MIT | ||
|
||
// https://doc.rust-lang.org/std/panic/fn.catch_unwind.html | ||
// Stable way of calling the `try` intrinsic. | ||
use std::panic; | ||
|
||
fn main() { | ||
let result = panic::catch_unwind(|| { | ||
println!("hello!"); | ||
}); | ||
assert!(result.is_ok()); | ||
|
||
let result = panic::catch_unwind(|| { | ||
panic!("oh no!"); | ||
}); | ||
assert!(result.is_err()); | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,18 @@ | ||
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. | ||
// SPDX-License-Identifier: Apache-2.0 OR MIT | ||
|
||
// See discussion on https://github.com/model-checking/rmc/issues/267 | ||
#![feature(core_intrinsics)] | ||
use std::intrinsics::r#try; | ||
|
||
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"), | ||
); | ||
} | ||
} |