[ldv-project] Version 0.8 of LDV Tools released

[Vadim Mutilin]

LDV Tools 0.8 comes with the following improvements:

  * Update the CPAchecker verification tool to the new version 1.4
    (r14998) <http://cpachecker.sosy-lab.org/NEWS-1.4.txt>.
  * LDV Tools are now available as Docker images
    <http://forge.ispras.ru/projects/ldv/wiki/LDV_Tools_in_Docker>, so
    you can avoid installation of all dependencies on your machine.
  * Improvements in 13 existing rule specifications:
      o Driver becomes not available for unloading permanently
        <http://forge.ispras.ru/issues/3239>.
      o Locking a mutex twice or unlocking without prior locking
        <http://forge.ispras.ru/issues/1940>.
      o Usage of spin lock and unlock functions
        <http://forge.ispras.ru/issues/5349>.
      o Usb alloc/free urb <http://forge.ispras.ru/issues/3233>.
      o Possible TTY NULL dereference <http://forge.ispras.ru/issues/2692>.
      o Atomic allocation in interrupt context
        <http://forge.ispras.ru/issues/3317>.
      o Memory allocation inside spinlocks
        <http://forge.ispras.ru/issues/3232>.
      o NOIO allocation under usb_lock <http://forge.ispras.ru/issues/3220>.
      o Initialization of completion <http://forge.ispras.ru/issues/3865>.
      o Error handling in probe() <http://forge.ispras.ru/issues/3313>.
      o All obtained blk requests should be put after all
        <http://forge.ispras.ru/issues/2706>.
      o Calling find_next_zero_bit() with arguments in the right order
        <http://forge.ispras.ru/issues/3261>.
      o Usb device reference counting with usb_get_dev/usb_put_dev and
        interface_to_usbdev <http://forge.ispras.ru/issues/3306>.
  * Adding 3 new rule specifications:
      o Correct usage of sysfs groups <http://forge.ispras.ru/issues/5898>.
      o Correct usage of IO memory mappings
        <http://forge.ispras.ru/issues/5899>.
      o Correct allocation of identifiers using IDR layer
        <http://forge.ispras.ru/issues/5900>.

Results of validation 
<http://forge.ispras.ru/projects/ldv/wiki/LDV_Validator> 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

	BLAST 	CPAchecker 	BLAST 	CPAchecker
Found bugs 	*19* 	*18* 	*19* 	*15*
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 
<http://cpachecker.sosy-lab.org/NEWS-1.4.txt>.

The source code repository can be browsed by v0.8 
<http://forge.ispras.ru/projects/ldv/repository?utf8=%E2%9C%93&rev=v0.8> 
tag. To get and to install LDV Tools see instructions 
<http://forge.ispras.ru/projects/ldv/wiki/Downloading_and_Building_LDV>. 
If you want to use prebuilt LDV Tools, please follow our LDV Tools in 
Docker <http://forge.ispras.ru/projects/ldv/wiki/LDV_Tools_in_Docker> 
instructions.

-- 
Vadim Mutilin
Linux Verification Center, ISPRAS
web:http://linuxtesting.org
e-mail:mutilin at ispras.ru

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://linuxtesting.org/pipermail/ldv-project/attachments/20150514/7b083836/attachment.html>