Skip to main content

creusot_std/std/
intrinsics.rs

1use crate::prelude::*;
2#[cfg(creusot)]
3use crate::std::mem::{align_of_logic, size_of_logic};
4
5extern_spec! {
6    mod core {
7        mod intrinsics {
8            #[check(ghost)]
9            fn ub_checks() -> bool;
10
11            #[check(ghost)]
12            #[requires(false)]
13            unsafe fn unreachable() -> !;
14
15            #[erasure]
16            #[check(ghost)]
17            #[requires(b)]
18            unsafe fn assume(b: bool) {
19                if !b {
20                    unsafe { core::intrinsics::unreachable() }
21                }
22            }
23
24            // This intrinsic is used by the constant `SizedTypeProperties::SIZE`
25            #[check(terminates)]
26            #[ensures(result@ == size_of_logic::<T>())]
27            fn size_of<T>() -> usize;
28
29            // This intrinsic is used by the constant `SizedTypeProperties::ALIGN`
30            #[check(terminates)]
31            #[ensures(result == align_of_logic::<T>())]
32            fn align_of<T>() -> usize;
33        }
34    }
35}