Add unstable tag to pointer_offset and pointer_object

model-checking · Jul 5, 2024 · 71c8313 · 71c8313
1 parent 057aa83
commit 71c8313
Show file tree

Hide file tree

Showing 2 changed files with 28 additions and 4 deletions.
diff --git a/library/kani/src/mem.rs b/library/kani/src/mem.rs
@@ -299,16 +299,28 @@ pub(crate) fn is_initialized<T: ?Sized>(_ptr: *const T, _len: usize) -> 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(crate) fn pointer_object<T: ?Sized>(_ptr: *const T) -> usize {
+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(crate) fn pointer_offset<T: ?Sized>(_ptr: *const T) -> usize {
+pub fn pointer_offset<T: ?Sized>(_ptr: *const T) -> usize {
     kani_intrinsic()
 }
 

diff --git a/library/kani_core/src/mem.rs b/library/kani_core/src/mem.rs
@@ -307,16 +307,28 @@ macro_rules! kani_mem {
         }
 
         /// 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(crate) fn pointer_object<T: ?Sized>(_ptr: *const T) -> usize {
+        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(crate) fn pointer_offset<T: ?Sized>(_ptr: *const T) -> usize {
+        pub fn pointer_offset<T: ?Sized>(_ptr: *const T) -> usize {
             kani_intrinsic()
         }
     };