Linux Driver Verification

Pavel Shved wrote:

It turned out that CPAchecker, aside from being three times slower, found some errors in the drivers proved safe by BLAST.

It is not surprising keeping in mind that rerouting is implemented in BLAST itself.

Alexey Khoroshilov wrote:

It is not surprising keeping in mind that rerouting is implemented in BLAST itself.

I held the comparison on 32_1 rule implemented without the rerouter. Both with BLAST and CPAchecker.

That is good to know.
Which CPAChecker UNSAFEs are not present in BLAST?

Note that this is an plain model, not sequence_infinite. Therefore, while it could be the case described in bug #1018, this requires further investigation.

In the archive uploaded the "unsafes" BLAST misses (kernel 31.6) are

BLAST says unknown, CPAchecker says unsafe:

1. drivers/media/dvb/dvb-core/dvb-core.ko ldv_main5_plain_sorted_withcheck
2. drivers/media/dvb/dvb-usb/dvb-usb-af9005.ko ldv_main1_plain_sorted_withcheck
3. drivers/media/dvb/dvb-usb/dvb-usb-dw2102.ko ldv_main0_plain_sorted_withcheck
4. drivers/media/video/cpia.ko ldv_main0_plain_sorted_withcheck
5. drivers/media/video/cx231xx/cx231xx.ko ldv_main6_plain_sorted_withcheck

BLAST says safe, CPAchecker says unsafe:

1. drivers/media/common/saa7146.ko ldv_main0_plain_sorted_withcheck
2. drivers/media/common/saa7146_vv.ko ldv_main0_plain_sorted_withcheck
3. drivers/media/dvb/dvb-usb/dvb-usb-af9015.ko ldv_main0_plain_sorted_withcheck
4. drivers/media/dvb/dvb-usb/dvb-usb-cxusb.ko ldv_main0_plain_sorted_withcheck
5. drivers/media/dvb/dvb-usb/dvb-usb-dib0700.ko ldv_main0_plain_sorted_withcheck
6. drivers/media/dvb/dvb-usb/dvb-usb-gp8psk.ko ldv_main0_plain_sorted_withcheck
7. drivers/media/dvb/dvb-usb/dvb-usb-gp8psk.ko ldv_main1_plain_sorted_withcheck
8. drivers/media/dvb/dvb-usb/dvb-usb-vp7045.ko ldv_main0_plain_sorted_withcheck
9. drivers/media/dvb/dvb-usb/dvb-usb-vp7045.ko ldv_main1_plain_sorted_withcheck
10. drivers/media/dvb/firewire/firedtv.ko ldv_main1_plain_sorted_withcheck
11. drivers/media/dvb/firewire/firedtv.ko ldv_main4_plain_sorted_withcheck
12. drivers/media/dvb/frontends/bcm3510.ko ldv_main0_plain_sorted_withcheck
13. drivers/media/dvb/ttusb-dec/ttusb_dec.ko ldv_main0_plain_sorted_withcheck
14. drivers/media/video/au0828/au0828.ko ldv_main4_plain_sorted_withcheck
15. drivers/media/video/s2255drv.ko ldv_main0_plain_sorted_withcheck
16. drivers/media/video/zc0301/zc0301.ko ldv_main0_plain_sorted_withcheck

I analyzed drivers/media/dvb/dvb-usb/dvb-usb-cxusb.ko, and found out that CPAchecker's positive is false (see bug #1019). I guess, it is the reason of most of the CPAchecker's unsafes listed, so the investigation should be postponed.