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 #[requires(true)]
18 #[ensures(true)]
19 fn spin_loop() {}
20
21 #[check(ghost)]
22 #[requires(false)]
23 unsafe fn unreachable_unchecked() -> ! {
24 unreachable!()
25 }
26
27 #[cfg(feature = "nightly")]
28 #[check(ghost)]
29 #[ensures(result == value)]
30 fn must_use<T>(value: T) -> T {
31 value
32 }
33
34 #[check(ghost)]
35 #[ensures(result == if cond { true_val } else { false_val })]
36 fn select_unpredictable<T>(cond: bool, true_val: T, false_val: T) -> T;
37 }
38 }
39}