Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix visibility of some Kani intrinsics #3323

Merged
14 changes: 13 additions & 1 deletion library/kani/src/mem.rs
Original file line number Diff line number Diff line change
Expand Up @@ -300,7 +300,7 @@ unsafe fn has_valid_value<T: ?Sized>(_ptr: *const T) -> bool {
/// Check whether `len * size_of::<T>()` bytes are initialized starting from `ptr`.
#[rustc_diagnostic_item = "KaniIsInitialized"]
#[inline(never)]
pub fn is_initialized<T: ?Sized>(_ptr: *const T) -> bool {
pub(crate) fn is_initialized<T: ?Sized>(_ptr: *const T) -> bool {
kani_intrinsic()
}

Expand All @@ -311,13 +311,25 @@ fn assert_is_initialized<T: ?Sized>(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<T: ?Sized>(_ptr: *const T) -> usize {
kani_intrinsic()
}

/// 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<T: ?Sized>(_ptr: *const T) -> usize {
Expand Down
20 changes: 17 additions & 3 deletions library/kani_core/src/mem.rs
Original file line number Diff line number Diff line change
Expand Up @@ -306,7 +306,7 @@ macro_rules! kani_mem {
/// Check whether `len * size_of::<T>()` bytes are initialized starting from `ptr`.
#[rustc_diagnostic_item = "KaniIsInitialized"]
#[inline(never)]
pub fn is_initialized<T: ?Sized>(_ptr: *const T) -> bool {
pub(crate) fn is_initialized<T: ?Sized>(_ptr: *const T) -> bool {
kani_intrinsic()
}

Expand All @@ -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<T: ?Sized>(_ptr: *const T) -> usize {
pub(crate) fn pointer_object<T: ?Sized>(_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<T: ?Sized>(_ptr: *const T) -> usize {
pub(crate) fn pointer_offset<T: ?Sized>(_ptr: *const T) -> usize {
kani_intrinsic()
}
};
Expand Down
Loading