creusot_contracts/std/
intrinsics.rs

1use crate::prelude::*;
2
3extern_spec! {
4    mod core {
5        mod intrinsics {
6            #[check(ghost)]
7            fn ub_checks() -> bool;
8
9            #[check(ghost)]
10            #[requires(false)]
11            unsafe fn unreachable() -> !;
12
13            #[erasure]
14            #[check(ghost)]
15            #[requires(b)]
16            unsafe fn assume(b: bool) {
17                if !b {
18                    unsafe { core::intrinsics::unreachable() }
19                }
20            }
21        }
22    }
23}