Refactors contracts to be tool agnostic

Author: stogaru

library/Cargo.lock

@@ -482,12 +482,12 @@ impl<T: ?Sized> *const T {
         // overflow and that both pointers `self` and the result are in the same 
         // allocation 
         ((self.addr() as isize).checked_add(count).is_some() &&
-            kani::mem::same_allocation(self, self.wrapping_byte_offset(count)))
+            core::ub_checks::same_allocation(self, self.wrapping_byte_offset(count)))
     )]
     #[ensures(|&result|
         // The resulting pointer should either be unchanged or still point to the same allocation
         (self.addr() == result.addr()) ||
-        (kani::mem::same_allocation(self, result))
+        (core::ub_checks::same_allocation(self, result))
     )]
     pub const unsafe fn byte_offset(self, count: isize) -> Self {
         // SAFETY: the caller must uphold the safety contract for `offset`.
@@ -1034,12 +1034,12 @@ impl<T: ?Sized> *const T {
         // overflow and that both pointers `self` and the result are in the same 
         // allocation 
         ((self.addr() as isize).checked_add(count as isize).is_some() &&
-            kani::mem::same_allocation(self, self.wrapping_byte_add(count)))
+            core::ub_checks::same_allocation(self, self.wrapping_byte_add(count)))
     )]
     #[ensures(|&result|
         // The resulting pointer should either be unchanged or still point to the same allocation
         (self.addr() == result.addr()) ||
-        (kani::mem::same_allocation(self, result))
+        (core::ub_checks::same_allocation(self, result))
     )]
     pub const unsafe fn byte_add(self, count: usize) -> Self {
         // SAFETY: the caller must uphold the safety contract for `add`.
@@ -1178,12 +1178,12 @@ impl<T: ?Sized> *const T {
         // cause overflow and that both pointers `self` and the result are in the 
         // same allocation 
         ((self.addr() as isize).checked_sub(count as isize).is_some() &&
-            kani::mem::same_allocation(self, self.wrapping_byte_sub(count)))
+            core::ub_checks::same_allocation(self, self.wrapping_byte_sub(count)))
     )]
     #[ensures(|&result|
         // The resulting pointer should either be unchanged or still point to the same allocation
         (self.addr() == result.addr()) ||
-        (kani::mem::same_allocation(self, result))
+        (core::ub_checks::same_allocation(self, result))
     )]
     pub const unsafe fn byte_sub(self, count: usize) -> Self {
         // SAFETY: the caller must uphold the safety contract for `sub`.

library/core/src/ptr/const_ptr.rs

@@ -477,17 +477,17 @@ impl<T: ?Sized> *mut T {
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
     #[requires(
         // If count is zero, any pointer is valid including null pointer.
-        (count == 0) || 
+        (count == 0) ||
         // Else if count is not zero, then ensure that subtracting `count` doesn't 
         // cause overflow and that both pointers `self` and the result are in the 
         // same allocation 
-        ((self.addr() as isize).checked_add(count).is_some() && 
-            kani::mem::same_allocation(self, self.wrapping_byte_offset(count)))
+        ((self.addr() as isize).checked_add(count).is_some() &&
+            core::ub_checks::same_allocation(self, self.wrapping_byte_offset(count)))
     )]
     #[ensures(|&result|
         // The resulting pointer should either be unchanged or still point to the same allocation
         (self.addr() == result.addr()) ||
-        (kani::mem::same_allocation(self, result))
+        (core::ub_checks::same_allocation(self, result))
     )]
     pub const unsafe fn byte_offset(self, count: isize) -> Self {
         // SAFETY: the caller must uphold the safety contract for `offset`.
@@ -1102,17 +1102,17 @@ impl<T: ?Sized> *mut T {
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
     #[requires(
         // If count is zero, any pointer is valid including null pointer.
-        (count == 0) || 
+        (count == 0) ||
         // Else if count is not zero, then ensure that subtracting `count` doesn't 
         // cause overflow and that both pointers `self` and the result are in the 
         // same allocation 
-        ((self.addr() as isize).checked_add(count as isize).is_some() && 
-            kani::mem::same_allocation(self, self.wrapping_byte_add(count)))
+        ((self.addr() as isize).checked_add(count as isize).is_some() &&
+            core::ub_checks::same_allocation(self, self.wrapping_byte_add(count)))
     )]
     #[ensures(|&result|
         // The resulting pointer should either be unchanged or still point to the same allocation
         (self.addr() == result.addr()) ||
-        (kani::mem::same_allocation(self, result))
+        (core::ub_checks::same_allocation(self, result))
     )]
     pub const unsafe fn byte_add(self, count: usize) -> Self {
         // SAFETY: the caller must uphold the safety contract for `add`.
@@ -1248,17 +1248,17 @@ impl<T: ?Sized> *mut T {
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
     #[requires(
         // If count is zero, any pointer is valid including null pointer.
-        (count == 0) || 
+        (count == 0) ||
         // Else if count is not zero, then ensure that subtracting `count` doesn't 
         // cause overflow and that both pointers `self` and the result are in the 
         // same allocation 
-        ((self.addr() as isize).checked_sub(count as isize).is_some() && 
-            kani::mem::same_allocation(self, self.wrapping_byte_sub(count)))
+        ((self.addr() as isize).checked_sub(count as isize).is_some() &&
+            core::ub_checks::same_allocation(self, self.wrapping_byte_sub(count)))
     )]
     #[ensures(|&result|
         // The resulting pointer should either be unchanged or still point to the same allocation
         (self.addr() == result.addr()) ||
-        (kani::mem::same_allocation(self, result))
+        (core::ub_checks::same_allocation(self, result))
     )]
     pub const unsafe fn byte_sub(self, count: usize) -> Self {
         // SAFETY: the caller must uphold the safety contract for `sub`.