[ldv-project] Version 0.4 of LDV Tools released

[Evgeny Novikov]

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>