diff --git a/library/kani/src/mem.rs b/library/kani/src/mem.rs index f861f6b2ba25..f718c09ec38d 100644 --- a/library/kani/src/mem.rs +++ b/library/kani/src/mem.rs @@ -300,7 +300,7 @@ unsafe fn has_valid_value(_ptr: *const T) -> bool { /// Check whether `len * size_of::()` bytes are initialized starting from `ptr`. #[rustc_diagnostic_item = "KaniIsInitialized"] #[inline(never)] -pub fn is_initialized(_ptr: *const T) -> bool { +pub(crate) fn is_initialized(_ptr: *const T) -> bool { kani_intrinsic() } @@ -311,6 +311,12 @@ fn assert_is_initialized(ptr: *const T) -> bool { } /// Get the object ID of the given pointer. +#[doc(hidden)] +#[crate::unstable( + feature = "ghost-state", + issue = 3184, + reason = "experimental ghost state/shadow memory API" +)] #[rustc_diagnostic_item = "KaniPointerObject"] #[inline(never)] pub fn pointer_object(_ptr: *const T) -> usize { @@ -318,6 +324,12 @@ pub fn pointer_object(_ptr: *const T) -> usize { } /// Get the object offset of the given pointer. +#[doc(hidden)] +#[crate::unstable( + feature = "ghost-state", + issue = 3184, + reason = "experimental ghost state/shadow memory API" +)] #[rustc_diagnostic_item = "KaniPointerOffset"] #[inline(never)] pub fn pointer_offset(_ptr: *const T) -> usize { diff --git a/library/kani_core/src/mem.rs b/library/kani_core/src/mem.rs index bcf4cd2248a6..0b029ad53089 100644 --- a/library/kani_core/src/mem.rs +++ b/library/kani_core/src/mem.rs @@ -306,7 +306,7 @@ macro_rules! kani_mem { /// Check whether `len * size_of::()` bytes are initialized starting from `ptr`. #[rustc_diagnostic_item = "KaniIsInitialized"] #[inline(never)] - pub fn is_initialized(_ptr: *const T) -> bool { + pub(crate) fn is_initialized(_ptr: *const T) -> bool { kani_intrinsic() } @@ -320,16 +320,30 @@ macro_rules! kani_mem { } /// Get the object ID of the given pointer. + // TODO: Add this back later, as there is no unstable attribute here. + // #[doc(hidden)] + // #[crate::unstable( + // feature = "ghost-state", + // issue = 3184, + // reason = "experimental ghost state/shadow memory API" + // )] #[rustc_diagnostic_item = "KaniPointerObject"] #[inline(never)] - pub fn pointer_object(_ptr: *const T) -> usize { + pub(crate) fn pointer_object(_ptr: *const T) -> usize { kani_intrinsic() } /// Get the object offset of the given pointer. + // TODO: Add this back later, as there is no unstable attribute here. + // #[doc(hidden)] + // #[crate::unstable( + // feature = "ghost-state", + // issue = 3184, + // reason = "experimental ghost state/shadow memory API" + // )] #[rustc_diagnostic_item = "KaniPointerOffset"] #[inline(never)] - pub fn pointer_offset(_ptr: *const T) -> usize { + pub(crate) fn pointer_offset(_ptr: *const T) -> usize { kani_intrinsic() } };