creusot_contracts/std/
hint.rs

1use crate::prelude::*;
2
3extern_spec! {
4    mod std {
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    }
35}