Version 0.8 of LDV Tools released
- Update the CPAchecker verification tool to the new version 1.4.
- LDV Tools are now available as Docker images, so you can avoid installation of all dependencies on your machine.
- Improvements in 13 existing rule specifications:
- Driver becomes not available for unloading permanently.
- Locking a mutex twice or unlocking without prior locking.
- Usage of spin lock and unlock functions.
- Usb alloc/free urb.
- Possible TTY NULL dereference.
- Atomic allocation in interrupt context.
- Memory allocation inside spinlocks.
- NOIO allocation under usb_lock.
- Initialization of completion.
- Error handling in probe().
- All obtained blk requests should be put after all.
- Calling find_next_zero_bit() with arguments in the right order.
- Usb device reference counting with usb_get_dev/usb_put_dev and interface_to_usbdev.
- Adding 3 new rule specifications:
Results of validation of LDV Tools 0.8 and LDV Tools 0.7 with different verification tools on 41 known bugs in the Linux kernel are presented in the table below.
|LDV Tools 0.8||LDV Tools 0.7|
|Missed bugs||Due to bugs in verification tools||3||2||3||2|
|Out of memory (63 gigabytes)||2||0||1||2|
|Timeouts (50 minutes)||0||5||0||6|
|Due to other reasons||17||16||18||16|
The new version of CPAchecker was able to find three more reference bugs in Linux kernel thanks to improvements described here.