Skip to content

Commit 398729c

Browse files
Fix visibility of some Kani intrinsics (rust-lang#3323)
This PR fixes inadvertently exposing some of the unstable Kani intrinsics. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
1 parent 441451c commit 398729c

File tree

2 files changed

+30
-4
lines changed

2 files changed

+30
-4
lines changed

library/kani/src/mem.rs

Lines changed: 13 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -300,7 +300,7 @@ unsafe fn has_valid_value<T: ?Sized>(_ptr: *const T) -> bool {
300300
/// Check whether `len * size_of::<T>()` bytes are initialized starting from `ptr`.
301301
#[rustc_diagnostic_item = "KaniIsInitialized"]
302302
#[inline(never)]
303-
pub fn is_initialized<T: ?Sized>(_ptr: *const T) -> bool {
303+
pub(crate) fn is_initialized<T: ?Sized>(_ptr: *const T) -> bool {
304304
kani_intrinsic()
305305
}
306306

@@ -311,13 +311,25 @@ fn assert_is_initialized<T: ?Sized>(ptr: *const T) -> bool {
311311
}
312312

313313
/// Get the object ID of the given pointer.
314+
#[doc(hidden)]
315+
#[crate::unstable(
316+
feature = "ghost-state",
317+
issue = 3184,
318+
reason = "experimental ghost state/shadow memory API"
319+
)]
314320
#[rustc_diagnostic_item = "KaniPointerObject"]
315321
#[inline(never)]
316322
pub fn pointer_object<T: ?Sized>(_ptr: *const T) -> usize {
317323
kani_intrinsic()
318324
}
319325

320326
/// Get the object offset of the given pointer.
327+
#[doc(hidden)]
328+
#[crate::unstable(
329+
feature = "ghost-state",
330+
issue = 3184,
331+
reason = "experimental ghost state/shadow memory API"
332+
)]
321333
#[rustc_diagnostic_item = "KaniPointerOffset"]
322334
#[inline(never)]
323335
pub fn pointer_offset<T: ?Sized>(_ptr: *const T) -> usize {

library/kani_core/src/mem.rs

Lines changed: 17 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -306,7 +306,7 @@ macro_rules! kani_mem {
306306
/// Check whether `len * size_of::<T>()` bytes are initialized starting from `ptr`.
307307
#[rustc_diagnostic_item = "KaniIsInitialized"]
308308
#[inline(never)]
309-
pub fn is_initialized<T: ?Sized>(_ptr: *const T) -> bool {
309+
pub(crate) fn is_initialized<T: ?Sized>(_ptr: *const T) -> bool {
310310
kani_intrinsic()
311311
}
312312

@@ -320,16 +320,30 @@ macro_rules! kani_mem {
320320
}
321321

322322
/// Get the object ID of the given pointer.
323+
// TODO: Add this back later, as there is no unstable attribute here.
324+
// #[doc(hidden)]
325+
// #[crate::unstable(
326+
// feature = "ghost-state",
327+
// issue = 3184,
328+
// reason = "experimental ghost state/shadow memory API"
329+
// )]
323330
#[rustc_diagnostic_item = "KaniPointerObject"]
324331
#[inline(never)]
325-
pub fn pointer_object<T: ?Sized>(_ptr: *const T) -> usize {
332+
pub(crate) fn pointer_object<T: ?Sized>(_ptr: *const T) -> usize {
326333
kani_intrinsic()
327334
}
328335

329336
/// Get the object offset of the given pointer.
337+
// TODO: Add this back later, as there is no unstable attribute here.
338+
// #[doc(hidden)]
339+
// #[crate::unstable(
340+
// feature = "ghost-state",
341+
// issue = 3184,
342+
// reason = "experimental ghost state/shadow memory API"
343+
// )]
330344
#[rustc_diagnostic_item = "KaniPointerOffset"]
331345
#[inline(never)]
332-
pub fn pointer_offset<T: ?Sized>(_ptr: *const T) -> usize {
346+
pub(crate) fn pointer_offset<T: ?Sized>(_ptr: *const T) -> usize {
333347
kani_intrinsic()
334348
}
335349
};

0 commit comments

Comments
 (0)