Tracking: bugs found by Verus verification

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

Navigation Menu