Open-Source Projects: Issueshttps://forge.ispras.ru/https://forge.ispras.ru/favicon.ico?16490126692013-02-08T13:30:32ZOpen-Source Projects
Redmine Linux Driver Verification - Bug #3931 (New): ETV doesn't render indirect function call properlyhttps://forge.ispras.ru/issues/39312013-02-08T13:30:32ZMikhail Mandrykinmandrykin@ispras.ru
<p>For driver:<br /><pre>
linux-3.8-rc1 32_7a drivers/media/v4l2-core/videodev.ko ldv_main6_sequence_infinite_withcheck_stateful
</pre></p>
<p>ETV renders indirect function call<br /><code>err = func(file, cmd, parg);</code><br />in line 2401 of v4l2-ioctl.c.prepared as<br /><code>(*func)(file, cmd, parg)</code>.<br />Neither curly bracket nor indentation of the following code after the call are present. The corresponding error path (ErrorPath.txt) is attached.</p> C Instrumentation Framework - Feature #3465 (Open): Loop head macros supporthttps://forge.ispras.ru/issues/34652012-09-20T12:49:36ZMikhail Mandrykinmandrykin@ispras.ru
<p>There are some marco definitions intended for some specific list or queue traverses. For instance,<br /><pre>
#define skb_queue_walk_safe(queue, skb, tmp) \
for (skb = (queue)->next, tmp = skb->next; \
skb != (struct sk_buff *)(queue); \
skb = tmp, tmp = skb->next)
</pre><br />It's desirable sometimes to have some instructions executed at each iteration of such loops. Here, for example, this macro enables us to detect assignments to <code>skb</code> varaible which is useful in checking for double <code>skb</code> deallocations.<br /><pre>
skb_queue_walk_safe(tx_skb_queue, skb, tmp) {
if (...) {
...
kfree_skb(skb);
}
}
</pre></p> Linux Kernel Safety RuleDB - Feature #3314 (Closed): 135: msleep and some other functions take ti...https://forge.ispras.ru/issues/33142012-07-31T18:01:58ZMikhail Mandrykinmandrykin@ispras.ru
<p>We should check parameters of some functions from linux/delay.h and linux/sched.h (and maybe some other headers) for being previously converted with the use of <code>msecs_to_jiffies</code> or <code>jiffies_to_msecs functions</code>.<br />Sample bugfix commit id: d6b6225.</p> Linux Kernel Safety RuleDB - Feature #3313 (New): 134: Error handling for critical functions in p...https://forge.ispras.ru/issues/33132012-07-31T17:40:20ZMikhail Mandrykinmandrykin@ispras.ru
<p>There are several "critical" functions that should normally cause probe() to return nonzero value in case of unsuccessful call. Possible examples are dma_set_mask and usb_register_dev.<br />Sample commit in linux_stable fixing error handling for dma_set_mask: eb9a2a9.</p> Linux Kernel Safety RuleDB - Bug #3312 (Closed): 134: Error handling for critical functions in pr...https://forge.ispras.ru/issues/33122012-07-31T17:35:29ZMikhail Mandrykinmandrykin@ispras.ru
<p>There are several "critical" functions that should normally cause probe() to return nonzero value in case of unsuccessful call. Possible examples are <code>dma_set_mask</code> and <code>usb_register_dev</code>.<br />Sample commit in linux_stable fixing error handling for <code>dma_set_mask</code>: eb9a2a9.</p> Linux Kernel Safety RuleDB - Feature #3311 (Open): 133: Don't call function kfree_skb twice https://forge.ispras.ru/issues/33112012-07-31T16:11:57ZMikhail Mandrykinmandrykin@ispras.ru
<p><code>kfree_skb</code> function should not be called twice for the same skb buffer (thus causing a double free).<br />Sample commit id in linux-stable repo is 08f7de1.</p> Linux Kernel Safety RuleDB - Feature #3306 (Open): 132: Usb device reference counting with usb_ge...https://forge.ispras.ru/issues/33062012-07-30T16:13:48ZMikhail Mandrykinmandrykin@ispras.ru
<p>Proper reference counting should be performed for <code>struct usb_device</code> with the use of functions <code>usb_get_dev</code>/<code>usb_put_dev</code>.<br /><pre>
/**
* usb_get_dev - increments the reference count of the usb device structure
* @dev: the device being referenced
*
* Each live reference to a device should be refcounted.
*
* Drivers for USB interfaces should normally record such references in
* their probe() methods, when they bind to an interface, and release
* them by calling usb_put_dev(), in their disconnect() methods.
</pre><br />Usually the reference count is increased in <code>probe()</code> handler and decreased in <code>disconnect()</code>/<code>exit()</code> handler. It look like <code>interface_to_usbdev()</code> macro is often used in <code>probe()</code> handler to get the reference to <code>usb_device</code> by the reference to <code>usb_interface</code>.</p>
<p>So the rule may be initially formalized in the following way: after acquiring a reference to <code>struct usb_device</code> with <code>usb_interface</code> macro one should increase the corresponding reference counter with <code>usb_get_dev</code> and then decrease it with <code>usb_put_dev</code> at finalization.</p>
<p><strong>Links</strong></p>
<p>Sample bugfixes <a href="https://git.kernel.org/cgit/linux/kernel/git/stable/linux-stable.git/commit/?id=927c3fa" class="external">927c3fa</a></p> C Instrumentation Framework - Bug #3246 (Closed): After moving common aspects into separate files...https://forge.ispras.ru/issues/32462012-07-20T15:05:23ZMikhail Mandrykinmandrykin@ispras.ru
<p>Using 'NULL' macro in 100_1a rule model aspect lead to BLAST failure with the following message:</p>
<pre>
/home/schrodinger/benchmark/cpachecker/work/current--X--packed_drivers/100_1a--test-start_tty.tar.bz2--X--defaultlinux-3.4.4--X--
100_1a/linux-3.4.4/csd_deg_dscv/11/dscv_tempdir/rule-instrumentor/100_1a/common-model/ldv_common_model.c:11: Error: Cannot resolve variable NULL.
/home/schrodinger/benchmark/cpachecker/work/current--X--packed_drivers/100_1a--test-start_tty.tar.bz2--X--defaultlinux-3.4.4--X--100_1a/linux
-3.4.4/csd_deg_dscv/11/dscv_tempdir/rule-instrumentor/100_1a/common-model/ldv_common_model.c:19: Error: Cannot resolve variable NULL.
</pre>
<p>Previously the model was tested with no BLAST failure.</p>