@@ -235,7 +235,7 @@ impl Duration {
235
235
#[ must_use]
236
236
#[ inline]
237
237
#[ rustc_const_stable( feature = "duration_consts" , since = "1.32.0" ) ]
238
- // #[ensures(|duration| duration.is_safe())]
238
+ #[ ensures( |duration| duration. is_safe( ) ) ]
239
239
#[ ensures( |duration| duration. secs == secs) ]
240
240
pub const fn from_secs ( secs : u64 ) -> Duration {
241
241
Duration { secs, nanos : Nanoseconds :: ZERO }
@@ -511,7 +511,7 @@ impl Duration {
511
511
#[ rustc_const_stable( feature = "duration_consts" , since = "1.32.0" ) ]
512
512
#[ must_use]
513
513
#[ inline]
514
- #[ ensures( |ms| * ms == self . nanos. 0 / NANOS_PER_MILLI ) ]
514
+ #[ ensures( |ms| * ms == self . nanos. get_zero ( ) / NANOS_PER_MILLI ) ]
515
515
pub const fn subsec_millis ( & self ) -> u32 {
516
516
self . nanos . as_inner ( ) / NANOS_PER_MILLI
517
517
}
@@ -535,7 +535,7 @@ impl Duration {
535
535
#[ rustc_const_stable( feature = "duration_consts" , since = "1.32.0" ) ]
536
536
#[ must_use]
537
537
#[ inline]
538
- // #[ensures(|ms| *ms == self.nanos.0 / NANOS_PER_MICRO)]
538
+ #[ ensures( |ms| * ms == self . nanos. get_zero ( ) / NANOS_PER_MICRO ) ]
539
539
pub const fn subsec_micros ( & self ) -> u32 {
540
540
self . nanos . as_inner ( ) / NANOS_PER_MICRO
541
541
}
@@ -559,7 +559,7 @@ impl Duration {
559
559
#[ rustc_const_stable( feature = "duration_consts" , since = "1.32.0" ) ]
560
560
#[ must_use]
561
561
#[ inline]
562
- #[ ensures( |nanos| * nanos == self . nanos. 0 ) ]
562
+ #[ ensures( |nanos| * nanos == self . nanos. get_zero ( ) ) ]
563
563
pub const fn subsec_nanos ( & self ) -> u32 {
564
564
self . nanos . as_inner ( )
565
565
}
@@ -578,7 +578,7 @@ impl Duration {
578
578
#[ rustc_const_stable( feature = "duration_as_u128" , since = "1.33.0" ) ]
579
579
#[ must_use]
580
580
#[ inline]
581
- // #[ensures(|ms| *ms == self.secs as u128 * MILLIS_PER_SEC as u128 + (self.nanos.0 / NANOS_PER_MILLI) as u128)]
581
+ #[ ensures( |ms| * ms == self . secs as u128 * MILLIS_PER_SEC as u128 + ( self . nanos. get_zero ( ) / NANOS_PER_MILLI ) as u128 ) ]
582
582
pub const fn as_millis ( & self ) -> u128 {
583
583
self . secs as u128 * MILLIS_PER_SEC as u128
584
584
+ ( self . nanos . as_inner ( ) / NANOS_PER_MILLI ) as u128
@@ -598,7 +598,7 @@ impl Duration {
598
598
#[ rustc_const_stable( feature = "duration_as_u128" , since = "1.33.0" ) ]
599
599
#[ must_use]
600
600
#[ inline]
601
- #[ ensures( |ms| * ms == self . secs as u128 * MICROS_PER_SEC as u128 + ( self . nanos. 0 / NANOS_PER_MICRO ) as u128 ) ]
601
+ #[ ensures( |ms| * ms == self . secs as u128 * MICROS_PER_SEC as u128 + ( self . nanos. get_zero ( ) / NANOS_PER_MICRO ) as u128 ) ]
602
602
pub const fn as_micros ( & self ) -> u128 {
603
603
self . secs as u128 * MICROS_PER_SEC as u128
604
604
+ ( self . nanos . as_inner ( ) / NANOS_PER_MICRO ) as u128
@@ -716,7 +716,7 @@ impl Duration {
716
716
without modifying the original"]
717
717
#[ inline]
718
718
#[ rustc_const_stable( feature = "duration_consts_2" , since = "1.58.0" ) ]
719
- // #[ensures(|duration| duration.is_none() || duration.unwrap().is_safe())]
719
+ #[ ensures( |duration| duration. is_none( ) || duration. unwrap( ) . is_safe( ) ) ]
720
720
pub const fn checked_sub ( self , rhs : Duration ) -> Option < Duration > {
721
721
if let Some ( mut secs) = self . secs . checked_sub ( rhs. secs ) {
722
722
let nanos = if self . nanos . as_inner ( ) >= rhs. nanos . as_inner ( ) {
@@ -829,7 +829,7 @@ impl Duration {
829
829
#[ must_use = "this returns the result of the operation, \
830
830
without modifying the original"]
831
831
#[ inline]
832
- // #[ensures(|duration| rhs == 0 || duration.unwrap().is_safe())]
832
+ #[ ensures( |duration| rhs == 0 || duration. unwrap( ) . is_safe( ) ) ]
833
833
#[ rustc_const_stable( feature = "duration_consts_2" , since = "1.58.0" ) ]
834
834
pub const fn checked_div ( self , rhs : u32 ) -> Option < Duration > {
835
835
if rhs != 0 {
0 commit comments