clippy

model-checking · Jul 10, 2024 · 52d3839 · 52d3839
1 parent c28bad7
commit 52d3839
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 13 deletions.
diff --git a/library/kani/src/internal.rs b/library/kani/src/internal.rs
@@ -27,7 +27,6 @@ impl<'a, 'b, T: ?Sized> Pointer<'a> for &'b T {
  std::mem::transmute(*self)
  }
 
- #[allow(clippy::transmute_ptr_to_ref)]
  unsafe fn assignable(self) -> *mut Self::Inner {
  std::mem::transmute(self as *const T)
  }
@@ -42,7 +41,7 @@ impl<'a, 'b, T: ?Sized> Pointer<'a> for &'b mut T {
  }
 
  unsafe fn assignable(self) -> *mut Self::Inner {
- std::mem::transmute(self)
+ self as *mut T
  }
 }
 
@@ -52,7 +51,6 @@ impl<'a, T: ?Sized> Pointer<'a> for *const T {
  &**self as &'a T
  }
 
- #[allow(clippy::transmute_ptr_to_ref)]
  unsafe fn assignable(self) -> *mut Self::Inner {
  std::mem::transmute(self)
  }
@@ -64,9 +62,8 @@ impl<'a, T: ?Sized> Pointer<'a> for *mut T {
  &**self as &'a T
  }
 
- #[allow(clippy::transmute_ptr_to_ref)]
  unsafe fn assignable(self) -> *mut Self::Inner {
- std::mem::transmute(self)
+ self
  }
 }
 
@@ -123,7 +120,7 @@ pub fn any_modifies<T>() -> T {
 #[rustc_diagnostic_item = "KaniWriteAny"]
 #[inline(never)]
 #[doc(hidden)]
-pub fn write_any<T: ?Sized>(_pointer: *mut T) {
+pub unsafe fn write_any<T: ?Sized>(_pointer: *mut T) {
  // This function should not be reacheable.
  // Users must include `#[kani::recursion]` in any function contracts for recursive functions;
  // otherwise, this might not be properly instantiate. We mark this as unreachable to make
@@ -134,21 +131,21 @@ pub fn write_any<T: ?Sized>(_pointer: *mut T) {
 #[crate::unstable(feature = "function-contracts", issue = "none", reason = "function-contracts")]
 #[rustc_diagnostic_item = "KaniWriteAnySlice"]
 #[inline(always)]
-pub fn write_any_slice<T: Arbitrary>(slice: *mut [T]) {
- unsafe { (*slice).fill_with(T::any) }
+pub unsafe fn write_any_slice<T: Arbitrary>(slice: *mut [T]) {
+ (*slice).fill_with(T::any)
 }
 
 #[crate::unstable(feature = "function-contracts", issue = "none", reason = "function-contracts")]
 #[rustc_diagnostic_item = "KaniWriteAnySlim"]
 #[inline(always)]
-pub fn write_any_slim<T: Arbitrary>(pointer: *mut T) {
- unsafe { ptr::write(pointer, T::any()) }
+pub unsafe fn write_any_slim<T: Arbitrary>(pointer: *mut T) {
+ ptr::write(pointer, T::any())
 }
 
 #[crate::unstable(feature = "function-contracts", issue = "none", reason = "function-contracts")]
 #[rustc_diagnostic_item = "KaniWriteAnyStr"]
 #[inline(always)]
-pub fn write_any_str(s: *mut str) {
- unsafe { (*s).as_bytes_mut() }.fill_with(u8::any)
+pub unsafe fn write_any_str(s: *mut str) {
+ (*s).as_bytes_mut().fill_with(u8::any)
  //TODO: String validation
 }
diff --git a/library/kani_macros/src/sysroot/contracts/replace.rs b/library/kani_macros/src/sysroot/contracts/replace.rs
@@ -99,7 +99,7 @@ impl<'a> ContractConditionsHandler<'a> {
  let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site());
  quote!(
  #(#before)*
- #(kani::internal::write_any(unsafe{kani::internal::Pointer::assignable(kani::internal::untracked_deref(&#attr))});)*
+ #(unsafe{kani::internal::write_any(kani::internal::Pointer::assignable(kani::internal::untracked_deref(&#attr)))};)*
  #(#after)*
  #result
  )