<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html>
<head>
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
</head>
<body bgcolor="#ffffff" text="#000000">
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 <a
href="http://forge.ispras.ru/projects/ldv/repository"
class="external">LDV Tools repository</a> not including
submodules. The most significant changes are:
<ul>
<li>Improvements in existing rule models: <a
href="http://forge.ispras.ru/issues/3239" class="external">Module
get/put</a>, <a href="http://forge.ispras.ru/issues/3317"
class="external">Atomic allocation in interrupt context</a>, <a
href="http://forge.ispras.ru/issues/1940" class="external">Mutex
lock/unlock</a>, <a href="http://forge.ispras.ru/issues/3232"
class="external">Memory allocation under spinlocks</a>, <a
href="http://forge.ispras.ru/issues/3220" class="external">NOIO
allocation under USB lock</a>.</li>
<li>Support of 25 new rule models: <a
href="http://forge.ispras.ru/issues/2692" class="external">Possible
TTY NULL dereference</a>, <a
href="http://forge.ispras.ru/issues/2706" class="external">Block
requests</a>, <a href="http://forge.ispras.ru/issues/2732"
class="external">Usage of msleep()</a>, <a
href="http://forge.ispras.ru/issues/2742" class="external">USB
gadget driver (de)registration</a>, <a
href="http://forge.ispras.ru/issues/2747" class="external">Initialization
of spinlocks</a>, <a
href="http://forge.ispras.ru/issues/2771" class="external">Integer
underflow in calling copy_from_user(), copy_to_user(), etc.</a>,
<a href="http://forge.ispras.ru/issues/3035" class="external">Usage
of spin_lock_irq*()</a>, <a
href="http://forge.ispras.ru/issues/3223" class="external">Usage
of local_irq_*()</a>, <a
href="http://forge.ispras.ru/issues/3193" class="external">RW
locks lock/unlock</a>, <a
href="http://forge.ispras.ru/issues/2606" class="external">probe()
return values</a>, <a
href="http://forge.ispras.ru/issues/3261" class="external">Arguments
of find_next_zero_bit()</a>, <a
href="http://forge.ispras.ru/issues/3270" class="external">Initialization
of sysfs attributes</a>, <a
href="http://forge.ispras.ru/issues/3306" class="external">USB
reference counting</a>, <a
href="http://forge.ispras.ru/issues/3311" class="external">Double
kfree_skb()</a>, <a href="http://forge.ispras.ru/issues/3313"
class="external">Error handling in probe()</a>, <a
href="http://forge.ispras.ru/issues/3316" class="external">usb_deregister()
and usb_serial_deregister()</a>, <a
href="http://forge.ispras.ru/issues/3327" class="external">netif_napi_add()/netif_napi_del()</a>,
<a href="http://forge.ispras.ru/issues/3328" class="external">napi_enable()/napi_disable()</a>,
<a href="http://forge.ispras.ru/issues/3338" class="external">register_netdev()/unregister_netdev(),
alloc_netdev()/free_netdev()</a>, <a
href="http://forge.ispras.ru/issues/3340" class="external">Usage
of mod_timer()</a>, <a
href="http://forge.ispras.ru/issues/3399" class="external">Usage
of semaphores</a>, <a
href="http://forge.ispras.ru/issues/3608" class="external">Work
with clocks</a>, <a href="http://forge.ispras.ru/issues/3831"
class="external">RCU read sections nesting</a>, <a
href="http://forge.ispras.ru/issues/3832" class="external">RCU
update operations inside read sections</a>, <a
href="http://forge.ispras.ru/issues/3865" class="external">Initialization
of completions</a>.</li>
<li>Fixing patterns for several driver callback structures to
generate correct environment models.</li>
<li>Introducing <a href="http://forge.ispras.ru/projects/cif"
class="external">C Instrumentation Framework</a> - a
user-friendly interface for Aspectator.</li>
<li>Supporting reusable blocks of aspect files and corresponding
rearranging all existing rule models.</li>
<li>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 <a
href="http://forge.ispras.ru/news/184" class="external">news</a>)
and in generation of environment models.</li>
<li>Support of a more user-friendly interface for reachability C
verifiers.</li>
<li>Switch to <a href="http://forge.ispras.ru/news/126"
class="external">2.7.1</a> version of <a
href="http://forge.ispras.ru/projects/blast/" class="external">BLAST</a>
- a default verifier of LDV Tools.</li>
<li>Better integration with <a
href="http://cpachecker.sosy-lab.org/" class="external">CPAchecker</a>
verifier that was included as <a
href="http://forge.ispras.ru/projects/ldv/repository/changes/dscv/rcv/backends/cpachecker?rev=master"
class="external">submodule</a> of LDV Tools.</li>
<li>Integration with <a
href="https://bitbucket.org/arieg/ufo/wiki/Home"
class="external">UFO</a> verifier.</li>
<li>Introducing a common format of error traces and improving
visualization of error traces of different verifiers.</li>
<li><a href="http://forge.ispras.ru/news/69" class="external">Knowledge
Base</a> support for automatic marking unsafe verdicts of
verifiers.</li>
<li>Support for an automatic validation of LDV Tools and verifiers
on known bugs in the Linux kernel.</li>
<li>Coverage generation for debugging LDV Tools and different
analyses of CPAchecker verifier.</li>
</ul>
<a href="http://forge.ispras.ru/projects/ldv/wiki/LDV_Validator"
class="external">Validation</a> of LDV Tools 0.4 with different
verifiers on 38 known bugs in the Linux kernel showed that:
<ul>
<li>BLAST is able to detect 15 of them.</li>
<li>CPAchecker is able to detect 13 of them.</li>
</ul>
<p>The source code repository may be browsed by <a
href="http://forge.ispras.ru/projects/ldv/repository/show?rev=v0.4"
class="external">v0.4</a> tag. To get and to install LDV Tools
see <a
href="http://forge.ispras.ru/projects/ldv/wiki/Downloading_and_Building_LDV"
class="external">instructions</a>.<br>
</p>
<p>Source <a href="http://forge.ispras.ru/news/261">ISP RAS
Open-Source Projects</a>.</p>
<pre class="moz-signature" cols="72">--
Best regards, Evgeny Novikov.
Linux Verification Center, ISPRAS
web: <a class="moz-txt-link-freetext" href="http://linuxtesting.org">http://linuxtesting.org</a>
e-mail: <a class="moz-txt-link-abbreviated" href="mailto:novikov@ispras.ru">novikov@ispras.ru</a></pre>
</body>
</html>