11-Oct-2013: Version 0.4 of LDV Tools released

After more then 2 years of active development we are happy to announce that we released LDV Tools 0.4. This version includes a lot of improvements and many bug fixes. In total it consists of about 900 commits that were made just in the LDV Tools repository not including submodules. The most significant changes are:

• Improvements in existing rule specifications:
  • Module get/put
  • Atomic allocation in interrupt context
  • Mutex lock/unlock
  • Memory allocation under spinlocks
  • NOIO allocation under USB lock
• Support of 25 new rule specifications:
  • Possible TTY NULL dereference
  • Block requests
  • Usage of msleep()
  • USB gadget driver (de)registration
  • Initialization of spinlocks
  • Integer underflow in calling copy_from_user(), copy_to_user(), etc.
  • Usage of spin_lock_irq*()
  • Usage of local_irq_*()
  • RW locks lock/unlock
  • probe() return values
  • Arguments of find_next_zero_bit()
  • Initialization of sysfs attributes
  • USB reference counting
  • Double kfree_skb()
  • Error handling in probe()
  • usb_deregister() and usb_serial_deregister()
  • netif_napi_add()/netif_napi_del()
  • napi_enable()/napi_disable()
  • register_netdev()/unregister_netdev(), alloc_netdev()/free_netdev()
  • Usage of mod_timer()
  • Usage of semaphores
  • Work with clocks
  • RCU read sections nesting
  • RCU update operations inside read sections
  • Initialization of completions
• Fixing patterns for several driver callback structures to generate correct environment models.
• Introducing C Instrumentation Framework - a user-friendly interface for Aspectator.
• Supporting reusable blocks of aspect files and corresponding rearranging all existing rule specifications.
• Added ability to make source code querying with help of Aspectator, which is used in construction of rule specifications on the basis of instrumented source code (see corresponding news) and in generation of environment models.
• Support of a more user-friendly interface for reachability C verifiers.
• Switch to 2.7.1 version of BLAST - a default verifier of LDV Tools.
• Better integration with CPAchecker verifier that was included as submodule of LDV Tools.
• Integration with UFO verifier.
• Introducing a common format of error traces and improving visualization of error traces of different verifiers.
• Knowledge Base support for automatic marking unsafe verdicts of verifiers.
• Support for an automatic validation of LDV Tools and verifiers on known bugs in the Linux kernel.
• Coverage generation for debugging LDV Tools and different analyses of CPAchecker verifier.

Validation of LDV Tools 0.4 with different verifiers on 38 known bugs in the Linux kernel showed that:

• BLAST is able to detect 11 of them.
• CPAchecker is able to detect 10 of them.

The source code repository can be browsed by v0.4 tag. To get and to install LDV Tools see instructions.