@@ -45,7 +45,7 @@ macro_rules! declare_id {
4545 // We use 0 as a sentinel value (see the comment above) and,
4646 // therefore, need to shift by one when converting from an index
4747 // into a vector.
48- let shifted_idx = u32 :: try_from( idx) . unwrap( ) . checked_add ( 1 ) . unwrap ( ) ;
48+ let shifted_idx = u32 :: try_from( idx) . unwrap( ) . strict_add ( 1 ) ;
4949 $name( std:: num:: NonZero :: new( shifted_idx) . unwrap( ) )
5050 }
5151 fn index( self ) -> usize {
@@ -350,7 +350,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
350350 } else {
351351 mutex. owner = Some ( thread) ;
352352 }
353- mutex. lock_count = mutex. lock_count . checked_add ( 1 ) . unwrap ( ) ;
353+ mutex. lock_count = mutex. lock_count . strict_add ( 1 ) ;
354354 if let Some ( data_race) = & this. machine . data_race {
355355 data_race. acquire_clock ( & mutex. clock , & this. machine . threads ) ;
356356 }
@@ -370,9 +370,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
370370 return Ok ( None ) ;
371371 }
372372 let old_lock_count = mutex. lock_count ;
373- mutex. lock_count = old_lock_count
374- . checked_sub ( 1 )
375- . expect ( "invariant violation: lock_count == 0 iff the thread is unlocked" ) ;
373+ mutex. lock_count = old_lock_count. strict_sub ( 1 ) ;
376374 if mutex. lock_count == 0 {
377375 mutex. owner = None ;
378376 // The mutex is completely unlocked. Try transferring ownership
@@ -450,7 +448,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
450448 trace ! ( "rwlock_reader_lock: {:?} now also held (one more time) by {:?}" , id, thread) ;
451449 let rwlock = & mut this. machine . sync . rwlocks [ id] ;
452450 let count = rwlock. readers . entry ( thread) . or_insert ( 0 ) ;
453- * count = count. checked_add ( 1 ) . expect ( "the reader counter overflowed" ) ;
451+ * count = count. strict_add ( 1 ) ;
454452 if let Some ( data_race) = & this. machine . data_race {
455453 data_race. acquire_clock ( & rwlock. clock_unlocked , & this. machine . threads ) ;
456454 }
0 commit comments