Skip to content

Commit 968027e

Browse files
committed
Add extern_spec for Option::unwrap and Result::unwrap
1 parent d93148e commit 968027e

1 file changed

Lines changed: 14 additions & 0 deletions

File tree

std.rs

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -13,3 +13,17 @@ fn _extern_spec_box_new<T>(x: T) -> Box<T> {
1313
fn _extern_spec_std_mem_swap<T>(x: &mut T, y: &mut T) {
1414
std::mem::swap(x, y);
1515
}
16+
17+
#[thrust::extern_spec_fn]
18+
#[thrust::requires(opt != std::option::Option::<T0>::None())]
19+
#[thrust::ensures(std::option::Option::<T0>::Some(result) == opt)]
20+
fn _extern_spec_option_unwrap<T>(opt: Option<T>) -> T {
21+
Option::unwrap(opt)
22+
}
23+
24+
#[thrust::extern_spec_fn]
25+
#[thrust::requires(exists x:T0. res == std::result::Result::<T0, T1>::Ok(x))]
26+
#[thrust::ensures(std::result::Result::<T0, T1>::Ok(result) == res)]
27+
fn _extern_spec_result_unwrap<T, E: std::fmt::Debug>(res: Result<T, E>) -> T {
28+
Result::unwrap(res)
29+
}

0 commit comments

Comments
 (0)