creusot_contracts/std/
hint.rs

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
use crate::*;

extern_spec! {
    mod std {
        mod hint {
            #[pure]
            #[requires(cond)]
            unsafe fn assert_unchecked(cond: bool) {}

            #[pure]
            #[ensures(result == dummy)]
            fn black_box<T>(dummy: T) -> T {
                dummy
            }

            #[pure]
            #[requires(true)]
            #[ensures(true)]
            fn spin_loop() {}

            #[pure]
            #[requires(false)]
            unsafe fn unreachable_unchecked() -> ! {
                unreachable!()
            }

            #[cfg(feature = "nightly")]
            #[pure]
            #[ensures(result == value)]
            fn must_use<T>(value: T) -> T {
                value
            }
        }
    }
}