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            #[rustc_comptime]
28            fn size_of<T>() -> usize;
29
30            // This intrinsic is used by the constant `SizedTypeProperties::ALIGN`
31            #[check(terminates)]
32            #[ensures(result == align_of_logic::<T>())]
33            #[rustc_comptime]
34            fn align_of<T>() -> usize;
35        }
36    }
37}
creusot_std/std/intrinsics.rs

creusot_std/std/
intrinsics.rs
