1use crate::prelude::*;
2
3extern_spec! {
4 mod core {
5 mod hint {
6 #[check(ghost)]
7 #[requires(cond)]
8 unsafe fn assert_unchecked(cond: bool) {}
9
10 #[check(ghost)]
11 #[ensures(result == dummy)]
12 fn black_box<T>(dummy: T) -> T {
13 dummy
14 }
15
16 #[check(ghost)]
17 fn spin_loop() {}
18
19 #[check(ghost)]
20 #[requires(false)]
21 unsafe fn unreachable_unchecked() -> ! {
22 unreachable!()
23 }
24
25 #[cfg(feature = "nightly")]
26 #[check(ghost)]
27 #[ensures(result == value)]
28 fn must_use<T>(value: T) -> T {
29 value
30 }
31
32 #[check(ghost)]
33 #[ensures(result == if cond { true_val } else { false_val })]
34 fn select_unpredictable<T>(cond: bool, true_val: T, false_val: T) -> T;
35 }
36 }
37}