Tracking: bugs found by Verus verification

[Marsman1996]

This list tracks bugs found through formal verification. Each entry is marked as , , or .

• Undefined behaviour in <Weak as NonNullPtr>::into_raw asterinas#2801
• Deadlock in RwLock::try_upgrade, fixed by Make try_upgrade private in RwLock and RwMutex asterinas#3007
• Deadlock in RwMutex::try_upgrade, fixed by Make try_upgrade private in RwLock and RwMutex asterinas#3007
• Missing panic condition in Cursor::jump, fixed by Fix Cursor::jump documentation asterinas#3166
• Arithmetic overflow in Segment::slice, fixed by Fix silent integer wrapping in Segment::slice asterinas#3587
• Arithmetic overflow in is_valid_range through VmSpace::cursor_mut, details in Bug: Possible overflow in is_valid_range #603 and fixed by asterinas#3610
• Arithmetic overflow in Cursor::find_next_impl, reported in asterinas#3159 and fixed by asterinas#3610
• Wrong safety condition of drop_meta_in_place, reported in (Refine the safety condition of drop_meta_in_place asterinas#3683)
• Arithmetic overflow in CursorMut::unmap, reported in asterinas#3159
• Arithmetic overflow in VmIo::write, reported in asterinas#3159
• Counter wraparound in WaitQueue, reported in Stale wakers in WaitQueue may cause unbounded growth and lost wakeups by flock or fcntl asterinas#3283
• Reachable debug_assert in KernelPtConfig::item_raw_info due to uncleaned AVAIL1, reported in asterinas/asterinas#3597