Fix regression after merge

- Simplify the Pointer structure a bit more
model-checking · Jul 25, 2024 · 5d28e22 · 5d28e22
1 parent e3d907f
commit 5d28e22
Show file tree

Hide file tree

Showing 2 changed files with 24 additions and 22 deletions.
diff --git a/library/kani/src/internal.rs b/library/kani/src/internal.rs
@@ -8,36 +8,38 @@ use std::ptr;
 ///
 /// We allow the user to provide us with a pointer-like object that we convert as needed.
 #[doc(hidden)]
-pub trait Pointer<'a> {
+pub trait Pointer {
     /// Type of the pointed-to data
     type Inner: ?Sized;
 
+    /// used for havocking on replecement of a `modifies` clause.
     unsafe fn assignable(self) -> *mut Self::Inner;
 }
 
-impl<'a, 'b, T: ?Sized> Pointer<'a> for &'b T {
+impl<T: ?Sized> Pointer for &T {
     type Inner = T;
     unsafe fn assignable(self) -> *mut Self::Inner {
-        std::mem::transmute(self as *const T)
+        self as *const T as *mut T
     }
 }
 
-impl<'a, 'b, T: ?Sized> Pointer<'a> for &'b mut T {
+impl<T: ?Sized> Pointer for &mut T {
     type Inner = T;
 
     unsafe fn assignable(self) -> *mut Self::Inner {
         self as *mut T
     }
 }
 
-impl<'a, T: ?Sized> Pointer<'a> for *const T {
+impl<T: ?Sized> Pointer for *const T {
     type Inner = T;
+
     unsafe fn assignable(self) -> *mut Self::Inner {
-        std::mem::transmute(self)
+        self as *mut T
     }
 }
 
-impl<'a, T: ?Sized> Pointer<'a> for *mut T {
+impl<T: ?Sized> Pointer for *mut T {
     type Inner = T;
     unsafe fn assignable(self) -> *mut Self::Inner {
         self

diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs
@@ -295,48 +295,48 @@ macro_rules! kani_intrinsics {
         }
 
         pub mod internal {
+            use crate::kani::Arbitrary;
+            use core::ptr;
 
             /// Helper trait for code generation for `modifies` contracts.
             ///
             /// We allow the user to provide us with a pointer-like object that we convert as needed.
             #[doc(hidden)]
-            pub trait Pointer<'a> {
+            pub trait Pointer {
                 /// Type of the pointed-to data
                 type Inner: ?Sized;
 
                 /// used for havocking on replecement of a `modifies` clause.
-                unsafe fn assignable(self) -> &'a mut Self::Inner;
+                unsafe fn assignable(self) -> *mut Self::Inner;
             }
 
-            impl<'a, 'b, T: ?Sized> Pointer<'a> for &'b T {
+            impl<T: ?Sized> Pointer for &T {
                 type Inner = T;
-                #[allow(clippy::transmute_ptr_to_ref)]
-                unsafe fn assignable(self) -> &'a mut Self::Inner {
-                    $core::mem::transmute(self as *const T)
+                unsafe fn assignable(self) -> *mut Self::Inner {
+                    self as *const T as *mut T
                 }
             }
 
-            impl<'a, 'b, T: ?Sized> Pointer<'a> for &'b mut T {
+            impl<T: ?Sized> Pointer for &mut T {
                 type Inner = T;
 
-                unsafe fn assignable(self) -> &'a mut Self::Inner {
-                    $core::mem::transmute(self)
+                unsafe fn assignable(self) -> *mut Self::Inner {
+                    self as *mut T
                 }
             }
 
-            impl<'a, T: ?Sized> Pointer<'a> for *const T {
+            impl<T: ?Sized> Pointer for *const T {
                 type Inner = T;
 
                 unsafe fn assignable(self) -> *mut Self::Inner {
-                    core::mem::transmute(self)
+                    self as *mut T
                 }
             }
 
-            impl<'a, T: ?Sized> Pointer<'a> for *mut T {
+            impl<T: ?Sized> Pointer for *mut T {
                 type Inner = T;
-                #[allow(clippy::transmute_ptr_to_ref)]
-                unsafe fn assignable(self) -> &'a mut Self::Inner {
-                    $core::mem::transmute(self)
+                unsafe fn assignable(self) -> *mut Self::Inner {
+                    self
                 }
             }