From ad404e049bf8f60915da4df0e62785680b71c497 Mon Sep 17 00:00:00 2001
From: Shoyu Vanilla <modulo641@gmail.com>
Date: Sun, 29 Dec 2024 04:12:25 +0900
Subject: [PATCH] Clean the codes a bit

---
 library/core/src/convert/num.rs | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/library/core/src/convert/num.rs b/library/core/src/convert/num.rs
index a93461a1d1d4c..e7bdf0495f45c 100644
--- a/library/core/src/convert/num.rs
+++ b/library/core/src/convert/num.rs
@@ -4,6 +4,9 @@ use safety::{ensures, requires};
 #[cfg(kani)]
 use crate::kani;
 
+#[allow(unused_imports)]
+use crate::ub_checks::float_to_int_in_range;
+
 mod private {
     /// This trait being unreachable from outside the crate
     /// prevents other implementations of the `FloatToInt` trait,
@@ -31,11 +34,8 @@ macro_rules! impl_float_to_int {
                 #[inline]
                 #[requires(
                     !self.is_nan() &&
-                    !self.is_infinite() &&
-                    // Even if <$Int>::MIN < <$Float>::MIN or <$Int>::MAX > <$Float>::MAX,
-                    // the bounds would be -Inf or Inf, so they'll work anyways
-                    self > <$Int>::MIN as $Float - 1.0 &&
-                    self < <$Int>::MAX as $Float + 1.0
+                    self.is_finite() &&
+                    ub_checks::float_to_int_in_range::<$Float, $Int>(self)
                 )]
                 #[ensures(|&result|{
                     let fract = self - result as $Float;