<html>
<head>
<meta http-equiv="content-type" content="text/html;
charset=ISO-8859-1">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<p>LDV Tools 0.8 comes with the following improvements:</p>
<ul>
<li>Update the CPAchecker verification tool to the new <a
href="http://cpachecker.sosy-lab.org/NEWS-1.4.txt">version 1.4
(r14998)</a>.</li>
<li>LDV Tools are now available as <a
href="http://forge.ispras.ru/projects/ldv/wiki/LDV_Tools_in_Docker">Docker
images</a>, so you can avoid installation of all dependencies
on your machine.</li>
<li>Improvements in 13 existing rule specifications:
<ul>
<li><a href="http://forge.ispras.ru/issues/3239">Driver
becomes not available for unloading permanently</a>.</li>
<li><a href="http://forge.ispras.ru/issues/1940">Locking a
mutex twice or unlocking without prior locking</a>.</li>
<li><a href="http://forge.ispras.ru/issues/5349">Usage of spin
lock and unlock functions</a>.</li>
<li><a href="http://forge.ispras.ru/issues/3233">Usb
alloc/free urb</a>.</li>
<li><a href="http://forge.ispras.ru/issues/2692">Possible TTY
NULL dereference</a>.</li>
<li><a href="http://forge.ispras.ru/issues/3317">Atomic
allocation in interrupt context</a>.</li>
<li><a href="http://forge.ispras.ru/issues/3232">Memory
allocation inside spinlocks</a>.</li>
<li><a href="http://forge.ispras.ru/issues/3220">NOIO
allocation under usb_lock</a>.</li>
<li><a href="http://forge.ispras.ru/issues/3865">Initialization
of completion</a>.</li>
<li><a href="http://forge.ispras.ru/issues/3313">Error
handling in probe()</a>.</li>
<li><a href="http://forge.ispras.ru/issues/2706">All obtained
blk requests should be put after all</a>.</li>
<li><a href="http://forge.ispras.ru/issues/3261">Calling
find_next_zero_bit() with arguments in the right order</a>.</li>
<li><a href="http://forge.ispras.ru/issues/3306">Usb device
reference counting with usb_get_dev/usb_put_dev and
interface_to_usbdev</a>.</li>
</ul>
</li>
<li>Adding 3 new rule specifications:
<ul>
<li><a href="http://forge.ispras.ru/issues/5898">Correct usage
of sysfs groups</a>.</li>
<li><a href="http://forge.ispras.ru/issues/5899">Correct usage
of IO memory mappings</a>.</li>
<li><a href="http://forge.ispras.ru/issues/5900">Correct
allocation of identifiers using IDR layer</a>.</li>
</ul>
</li>
</ul>
<p>Results of <a
href="http://forge.ispras.ru/projects/ldv/wiki/LDV_Validator">validation</a>
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.</p>
<table style="width: 70%; margin-left: 15%; margin-right: 15%;
text-align: center" border="1">
<tbody>
<tr>
<td colspan="2"><br>
</td>
<td colspan="2">LDV Tools 0.8</td>
<td colspan="2">LDV Tools 0.7</td>
</tr>
<tr>
<td colspan="2"><br>
</td>
<td>BLAST</td>
<td>CPAchecker</td>
<td>BLAST</td>
<td>CPAchecker</td>
</tr>
<tr>
<td colspan="2">Found bugs</td>
<td><b>19</b></td>
<td><b>18</b></td>
<td><b>19</b></td>
<td><b>15</b></td>
</tr>
<tr>
<td rowspan="4" style="vertical-align: middle">Missed bugs</td>
<td>Due to bugs in verification tools</td>
<td>3</td>
<td>2</td>
<td>3</td>
<td>2</td>
</tr>
<tr>
<td>Out of memory (63 gigabytes)</td>
<td>2</td>
<td>0</td>
<td>1</td>
<td>2</td>
</tr>
<tr>
<td>Timeouts (50 minutes)</td>
<td>0</td>
<td>5</td>
<td>0</td>
<td>6</td>
</tr>
<tr>
<td>Due to other reasons</td>
<td>17</td>
<td>16</td>
<td>18</td>
<td>16</td>
</tr>
</tbody>
</table>
<p>The new version of CPAchecker was able to find three more
reference bugs in Linux kernel thanks to improvements described <a
href="http://cpachecker.sosy-lab.org/NEWS-1.4.txt">here</a>.</p>
<p>The source code repository can be browsed by <a
href="http://forge.ispras.ru/projects/ldv/repository?utf8=%E2%9C%93&rev=v0.8">v0.8</a>
tag. To get and to install LDV Tools see <a
href="http://forge.ispras.ru/projects/ldv/wiki/Downloading_and_Building_LDV">instructions</a>.
If you want to use prebuilt LDV Tools, please follow our <a
href="http://forge.ispras.ru/projects/ldv/wiki/LDV_Tools_in_Docker">LDV
Tools in Docker</a> instructions.</p>
<pre class="moz-signature" cols="72">--
Vadim Mutilin
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">mutilin@ispras.ru</a></pre>
</body>
</html>