From 5d28e225408aaa48bf6260ef0ddddd63a6257bb7 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Thu, 25 Jul 2024 16:33:05 -0700
Subject: [PATCH] Fix regression after merge

- Simplify the Pointer structure a bit more
---
 library/kani/src/internal.rs | 16 +++++++++-------
 library/kani_core/src/lib.rs | 30 +++++++++++++++---------------
 2 files changed, 24 insertions(+), 22 deletions(-)

diff --git a/library/kani/src/internal.rs b/library/kani/src/internal.rs
index 6f90b171eb70..a6f2291cea08 100644
--- a/library/kani/src/internal.rs
+++ b/library/kani/src/internal.rs
@@ -8,21 +8,22 @@ 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 {
@@ -30,14 +31,15 @@ impl<'a, 'b, T: ?Sized> Pointer<'a> for &'b 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
index df026fce0ac1..d5ff9e3458ff 100644
--- 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
                 }
             }