safety -> kani

Author: thanhnguyen-aws

library/core/src/num/dec2flt/decimal_seq.rs

@@ -87,7 +87,7 @@ impl DecimalSeq {
         //
         // Trim is only called in `right_shift` and `left_shift`.
         debug_assert!(self.num_digits <= Self::MAX_DIGITS);
-        #[safety::loop_invariant(self.num_digits <= Self::MAX_DIGITS)]
+        #[cfg_attr(kani, kani::loop_invariant(self.num_digits <= Self::MAX_DIGITS))]
         while self.num_digits != 0 && self.digits[self.num_digits - 1] == 0 {
             self.num_digits -= 1;
         }
@@ -103,7 +103,7 @@ impl DecimalSeq {
         let dp = self.decimal_point as usize;
         let mut n = 0_u64;
 
-        #[safety::loop_invariant(n < 10u64.pow(kani::index as u32))]
+        #[cfg_attr(kani, kani::loop_invariant(n < 10u64.pow(kani::index as u32)))]
         for i in 0..dp {
             n *= 10;
             if i < self.num_digits {
@@ -136,14 +136,14 @@ impl DecimalSeq {
         let mut write_index = self.num_digits + num_new_digits;
         let mut n = 0_u64;
 
-        #[safety::loop_invariant(read_index <= Self::MAX_DIGITS &&
+        #[cfg_attr(kani, kani::loop_invariant(read_index <= Self::MAX_DIGITS &&
             write_index == read_index + num_new_digits &&
             n < 10u64 << (shift - 1) &&
             (n == 0 || write_index > 0) &&
             self.num_digits <= Self::MAX_DIGITS &&
             self.decimal_point <= self.num_digits as i32 &&
             forall!(|i in (0,DecimalSeq::MAX_DIGITS)| self.digits[i] <= 9)
-        )]
+        ))]
         while read_index != 0 {
             read_index -= 1;
             write_index -= 1;
@@ -158,7 +158,7 @@ impl DecimalSeq {
             n = quotient;
         }
 
-        #[safety::loop_invariant(self.num_digits <= Self::MAX_DIGITS && self.decimal_point <= self.num_digits as i32 && (write_index > 0 || prev(write_index) == 1))]
+        #[cfg_attr(kani, kani::loop_invariant(self.num_digits <= Self::MAX_DIGITS && self.decimal_point <= self.num_digits as i32 && (write_index > 0 || prev(write_index) == 1)))]
         while n > 0 {
             //true but hard to write proof with kani currently
             // kani::assume(write_index > 0);
@@ -188,15 +188,15 @@ impl DecimalSeq {
         let mut read_index = 0;
         let mut write_index = 0;
         let mut n = 0_u64;
-        #[safety::loop_invariant( n == 0 || (read_index > 0 && read_index <= self.num_digits + 64 - n.leading_zeros() as usize))]
+        #[cfg_attr(kani, kani::loop_invariant( n == 0 || (read_index > 0 && read_index <= self.num_digits + 64 - n.leading_zeros() as usize)))]
         while (n >> shift) == 0 {
             if read_index < self.num_digits {
                 n = (10 * n) + self.digits[read_index] as u64;
                 read_index += 1;
             } else if n == 0 {
                 return;
             } else {
-                #[safety::loop_invariant(n > 0 && read_index <= self.num_digits + 64 - n.leading_zeros() as usize && read_index > 0)]
+                #[cfg_attr(kani, kani::loop_invariant(n > 0 && read_index <= self.num_digits + 64 - n.leading_zeros() as usize && read_index > 0))]
                 while (n >> shift) == 0 {
                     n *= 10;
                     read_index += 1;
@@ -213,18 +213,18 @@ impl DecimalSeq {
             return;
         }
         let mask = (1_u64 << shift) - 1;
-        #[safety::loop_invariant(self.num_digits <= Self::MAX_DIGITS &&
+        #[cfg_attr(kani, kani::loop_invariant(self.num_digits <= Self::MAX_DIGITS &&
             write_index < read_index &&
             write_index < Self::MAX_DIGITS - self.num_digits.saturating_sub(read_index)
-        )]
+        ))]
         while read_index < self.num_digits {
             let new_digit = (n >> shift) as u8;
             n = (10 * (n & mask)) + self.digits[read_index] as u64;
             read_index += 1;
             self.digits[write_index] = new_digit;
             write_index += 1;
         }
-        #[safety::loop_invariant(write_index <= Self::MAX_DIGITS)]
+        #[cfg_attr(kani, kani::loop_invariant(write_index <= Self::MAX_DIGITS))]
         while n > 0 {
             let new_digit = (n >> shift) as u8;
             n = 10 * (n & mask);
@@ -387,7 +387,7 @@ fn number_of_digits_decimal_left_shift(d: &DecimalSeq, mut shift: usize) -> usiz
     let pow5_b = (0x7FF & x_b) as usize;
     let pow5 = &TABLE_POW5[pow5_a..];
 
-    #[safety::loop_invariant(true)]
+    #[cfg_attr(kani, kani::loop_invariant(true))]
     for (i, &p5) in pow5.iter().enumerate().take(pow5_b - pow5_a) {
         if i >= d.num_digits {
             return num_new_digits - 1;