[ldv-project] Version 0.4 of LDV Tools released

Tue Oct 22 16:06:10 MSK 2013

After more then 2 years of active development we are happy to announce 
that we released version 0.4 of LDV Tools. 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 
<http://forge.ispras.ru/projects/ldv/repository> not including 
submodules. The most significant changes are:
 * Improvements in existing rule models: Module get/put
 <http://forge.ispras.ru/issues/3239>, Atomic allocation in
 interrupt context <http://forge.ispras.ru/issues/3317>, Mutex
 lock/unlock <http://forge.ispras.ru/issues/1940>, Memory
 allocation under spinlocks <http://forge.ispras.ru/issues/3232>,
 NOIO allocation under USB lock <http://forge.ispras.ru/issues/3220>.
 * Support of 25 new rule models: Possible TTY NULL dereference
 <http://forge.ispras.ru/issues/2692>, Block requests
 <http://forge.ispras.ru/issues/2706>, Usage of msleep()
 <http://forge.ispras.ru/issues/2732>, USB gadget driver
 (de)registration <http://forge.ispras.ru/issues/2742>,
 Initialization of spinlocks <http://forge.ispras.ru/issues/2747>,
 Integer underflow in calling copy_from_user(), copy_to_user(),
 etc. <http://forge.ispras.ru/issues/2771>, Usage of
 spin_lock_irq*() <http://forge.ispras.ru/issues/3035>, Usage of
 local_irq_*() <http://forge.ispras.ru/issues/3223>, RW locks
 lock/unlock <http://forge.ispras.ru/issues/3193>, probe() return
 values <http://forge.ispras.ru/issues/2606>, Arguments of
 find_next_zero_bit() <http://forge.ispras.ru/issues/3261>,
 Initialization of sysfs attributes
 <http://forge.ispras.ru/issues/3270>, USB reference counting
 <http://forge.ispras.ru/issues/3306>, Double kfree_skb()
 <http://forge.ispras.ru/issues/3311>, Error handling in probe()
 <http://forge.ispras.ru/issues/3313>, usb_deregister() and
 usb_serial_deregister() <http://forge.ispras.ru/issues/3316>,
 netif_napi_add()/netif_napi_del()
 <http://forge.ispras.ru/issues/3327>, napi_enable()/napi_disable()
 <http://forge.ispras.ru/issues/3328>,
 register_netdev()/unregister_netdev(),
 alloc_netdev()/free_netdev() <http://forge.ispras.ru/issues/3338>,
 Usage of mod_timer() <http://forge.ispras.ru/issues/3340>, Usage
 of semaphores <http://forge.ispras.ru/issues/3399>, Work with
 clocks <http://forge.ispras.ru/issues/3608>, RCU read sections
 nesting <http://forge.ispras.ru/issues/3831>, RCU update
 operations inside read sections
 <http://forge.ispras.ru/issues/3832>, Initialization of
 completions <http://forge.ispras.ru/issues/3865>.
 * Fixing patterns for several driver callback structures to generate
 correct environment models.
 * Introducing C Instrumentation Framework
 <http://forge.ispras.ru/projects/cif> - a user-friendly interface
 for Aspectator.
 * Supporting reusable blocks of aspect files and corresponding
 rearranging all existing rule models.
 * Added ability to make source code querying with help of
 Aspectator, which is used in construction of rule models on the
 basis of instrumented source code (see corresponding news
 <http://forge.ispras.ru/news/184>) and in generation of
 environment models.
 * Support of a more user-friendly interface for reachability C
 verifiers.
 * Switch to 2.7.1 <http://forge.ispras.ru/news/126> version of BLAST
 <http://forge.ispras.ru/projects/blast/> - a default verifier of
 LDV Tools.
 * Better integration with CPAchecker
 <http://cpachecker.sosy-lab.org/> verifier that was included as
 submodule
 <http://forge.ispras.ru/projects/ldv/repository/changes/dscv/rcv/backends/cpachecker?rev=master>
 of LDV Tools.
 * Integration with UFO <https://bitbucket.org/arieg/ufo/wiki/Home>
 verifier.
 * Introducing a common format of error traces and improving
 visualization of error traces of different verifiers.
 * Knowledge Base <http://forge.ispras.ru/news/69> 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 <http://forge.ispras.ru/projects/ldv/wiki/LDV_Validator> of 
LDV Tools 0.4 with different verifiers on 38 known bugs in the Linux 
kernel showed that:
 * BLAST is able to detect 15 of them.
 * CPAchecker is able to detect 13 of them.
The source code repository may be browsed by v0.4 
<http://forge.ispras.ru/projects/ldv/repository/show?rev=v0.4> tag. To 
get and to install LDV Tools see instructions 
<http://forge.ispras.ru/projects/ldv/wiki/Downloading_and_Building_LDV>.
Source ISP RAS Open-Source Projects <http://forge.ispras.ru/news/261>.
-- 
Best regards, Evgeny Novikov.
Linux Verification Center, ISPRAS
web: http://linuxtesting.org
e-mail: novikov at ispras.ru
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://linuxtesting.org/pipermail/ldv-project/attachments/20131022/72cd7ecd/attachment.html>