Remove before contracts. Fix import in

Author: yew005

library/core/src/num/int_macros.rs

@@ -511,8 +511,8 @@ macro_rules! int_impl {
                       without modifying the original"]
         #[inline(always)]
         #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
-        #[kani::requires(!self.overflowing_add(rhs).1)]
-        #[kani::ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)]
+        #[requires(!self.overflowing_add(rhs).1)]
+        #[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)]
         pub const unsafe fn unchecked_add(self, rhs: Self) -> Self {
             assert_unsafe_precondition!(
                 check_language_ub,

library/core/src/num/mod.rs

@@ -5,6 +5,10 @@
 use crate::str::FromStr;
 use crate::ub_checks::assert_unsafe_precondition;
 use crate::{ascii, intrinsics, mem};
+use safety::{ensures, requires};
+
+#[cfg(kani)]
+use crate::kani;
 
 // Used because the `?` operator is not allowed in a const context.
 macro_rules! try_opt {
@@ -1585,9 +1589,6 @@ from_str_radix_size_impl! { i32 isize, u32 usize }
 #[cfg(target_pointer_width = "64")]
 from_str_radix_size_impl! { i64 isize, u64 usize }
 
-#[cfg(kani)]
-use crate::kani;
-
 #[unstable(feature = "kani", issue = "none")]
 mod verify {
     use super::*;

library/core/src/num/uint_macros.rs

@@ -558,8 +558,8 @@ macro_rules! uint_impl {
                       without modifying the original"]
         #[inline(always)]
         #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
-        #[kani::requires(!self.overflowing_add(rhs).1)]
-        #[kani::ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)]
+        #[requires(!self.overflowing_add(rhs).1)]
+        #[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)]
         pub const unsafe fn unchecked_add(self, rhs: Self) -> Self {
             assert_unsafe_precondition!(
                 check_language_ub,