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            #[check(ghost)]
25            #[logic_alias(discriminant_value_logic(*v))]
26            fn discriminant_value<T>(v: &T) -> <T as core::marker::DiscriminantKind>::Discriminant;
27
28            // This intrinsic is used by the constant `SizedTypeProperties::SIZE`
29            #[check(terminates)]
30            #[ensures(result@ == size_of_logic::<T>())]
31            #[rustc_comptime]
32            fn size_of<T>() -> usize;
33
34            // This intrinsic is used by the constant `SizedTypeProperties::ALIGN`
35            #[check(terminates)]
36            #[ensures(result == align_of_logic::<T>())]
37            #[rustc_comptime]
38            fn align_of<T>() -> usize;
39        }
40    }
41}
42
43#[logic(open, inline)]
44#[intrinsic("discriminant_value_logic")]
45pub fn discriminant_value_logic<T>(_: T) -> <T as core::marker::DiscriminantKind>::Discriminant {
46    dead
47}
creusot_std/std/intrinsics.rs

creusot_std/std/
intrinsics.rs
