Open-Source Projects: Issueshttps://forge.ispras.ru/https://forge.ispras.ru/favicon.ico?16490126692016-05-27T13:34:08ZOpen-Source Projects
Redmine Klever - Bug #7260 (Closed): EMG does not generate a call for a handlerhttps://forge.ispras.ru/issues/72602016-05-27T13:34:08ZPavel Andrianovandrianov@ispras.ru
<p>In the driver drivers/net/wireless/ath/wil6210/wil6210.ko Linux 4.5-rc7 the handler wil_write_file_reset is not called. The old New DEG generated a call for this function.</p> Klever - Bug #7258 (Rejected): BCE fails while building Linux kernel v. 4.5https://forge.ispras.ru/issues/72582016-05-26T15:41:06ZPavel Andrianovandrianov@ispras.ru
<p>BCE fails with message<br />In file included from /usr/include/openssl/bio.h:62:0, from scripts/sign-file.c:24: /usr/include/openssl/e_os2.h:56:33: fatal error: openssl/opensslconf.h: No such file or directory compilation terminated.</p>
<p>The lib openssl is installed and ordinary 'make' in kernel directory successfully finishes.</p> Klever - Bug #7199 (Closed): EMG generates release() after all callbackshttps://forge.ispras.ru/issues/71992016-05-13T09:05:48ZPavel Andrianovandrianov@ispras.ru
<p>For validator 60b35930067d~ EMG generates strange model: after all callbacks there is a release function call. It also frees all available resources after every callback call.</p> Klever - Feature #7190 (Rejected): Add a case for nondet return in the main loophttps://forge.ispras.ru/issues/71902016-05-11T08:17:22ZPavel Andrianovandrianov@ispras.ru
<p>The current version of environment model does not finish, there is an infinite loop. Some analyses do not like it, particularly, the race analysis. There should be a way to the exit of the program without calling special function, like 'exit(0)'. Let it be an option to EMG to add one more case for nondeterministic return.</p> Klever - Bug #7141 (Closed): Factory process does not consider number of possible child instances https://forge.ispras.ru/issues/71412016-04-27T10:54:25ZPavel Andrianovandrianov@ispras.ru
<p>Factory process contains predefined number of child instances to register, but actual number of them can exceed the value (2). <br />Unsafe cannot be found in drivers/media/usb/dvb-usb/dvb-usb-cxusb.ko, callback emgfsa_state_10 is not called.</p> Linux Driver Verification - Task #5808 (New): Слишком большой драйвер btrfshttps://forge.ispras.ru/issues/58082015-04-07T09:32:06ZPavel Andrianovandrianov@ispras.ru
<p>Ошибка в функции btrfs_sync_log: в 158229 строке вызывается модельная функция ldv_blk_start_plug, но в ветке if в 158337 - 158343 строках отсутствует парная ей функция ldv_blk_finish_plug. Соответственно, в ldv_check_final_state счетчик должен быть равен единице, и вердит быть равным FALSE. При запуске LocationCPA-CallstackCPA + BAMCPA (то есть без всех анализов) и без метки ошибки анализ завершается через пару минут. Покрытие больше 50% - около 60 000 locations. Без функциональных указателей! При попытке включить какой-нибудь анализ, чтобы потом напечатался путь к ошибке, анализ падает с таймаутом. Смена точки входа на btrfs_sync_log не помогает - все равно покрытие оказывается слишком велико.</p> Linux Kernel Safety RuleDB - Feature #5365 (New): 202: All allocated memory from DMA pool should ...https://forge.ispras.ru/issues/53652014-10-20T10:44:06ZPavel Andrianovandrianov@ispras.ru
Memory from DMA pool is allocated by function <em>dma_pool_alloc</em>. The allocated memory is freed by function <em>dma_pool_free</em>. The rules of correct usage are:
<ul>
<li>freeing all allocated memory to avoid a memory leak;</li>
<li>freeing an allocated memory only once;</li>
<li>freeing only allocated memory.</li>
</ul> Linux Kernel Safety RuleDB - Feature #5364 (New): 204: DMA maps for PCI deviceshttps://forge.ispras.ru/issues/53642014-10-20T10:31:47ZPavel Andrianovandrianov@ispras.ru
DMA map for PCI device is created by the function <em>pci_map_single(struct pci_dev *, void *, size_t, int)</em> if its first argument is a correct pointer to a structure of PCI device. A DMA map is destroyed by function <em>pci_unmap_single(struct pci_dev *, dma_addr_t, size_t, int)</em>. The correct usage includes:
<ul>
<li>unmap only created maps;</li>
<li>create only one map for particular device;</li>
<li>cancel all created maps on module uploading.</li>
</ul>
<p>Sample bugfixes<br /><a href="https://git.kernel.org/cgit/linux/kernel/git/stable/linux-stable.git/commit/?id=468e4e3" class="external">468e4e3</a></p> Linux Kernel Safety RuleDB - Feature #5363 (New): 206: all created kernel threads should be stoppedhttps://forge.ispras.ru/issues/53632014-10-20T10:18:57ZPavel Andrianovandrianov@ispras.ru
Kernel threads are created by function <em>kthread_create</em>, which returns a pointer to a process structure, and are destroyed by <em>kthread_stop</em>. The rules of correct usage are:
<ul>
<li>destroying all created kernel threads;</li>
<li>destroying a created kernel thread only once;</li>
<li>destroying only created kernel thread.</li>
</ul>
<p><strong>Sample bugfix</strong></p>
<p><a href="https://git.kernel.org/cgit/linux/kernel/git/stable/linux-stable.git/commit/?id=efa73f1" class="external">efa73f1</a></p> Linux Kernel Safety RuleDB - Feature #5362 (New): 201: All allocated cache memory should be freedhttps://forge.ispras.ru/issues/53622014-10-20T09:48:34ZPavel Andrianovandrianov@ispras.ru
Cache memory is allocated by function <em>kmem_cache_alloc</em>, which takes a start of memory region and its size. The allocated memory region is freed by function <em>kmem_cache_free</em>. The rules of correct usage are:
<ul>
<li>freeing all allocated cache memory to avoid a memory leak;</li>
<li>freeing an allocated cache memory only once;</li>
<li>freeing only allocated cache memory.</li>
</ul>
<p>Sample bugfixes:<br /><a href="https://git.kernel.org/cgit/linux/kernel/git/stable/linux-stable.git/commit/?id=6a815cf" class="external">6a815cf</a></p> Linux Kernel Safety RuleDB - Feature #5357 (New): 203: All allocated IO-memory should be freedhttps://forge.ispras.ru/issues/53572014-10-20T09:04:55ZPavel Andrianovandrianov@ispras.ru
The region of memory is allocated by macrofunction <em>request_mem_region(start, n, name)</em>, which takes a start of memory region and its size. The allocated memory region is freed by macrofunction <em>release_mem_region(start, n)</em>. The rules of correct usage are:
<ul>
<li>freeing all allocated regions to avoid a memory leak;</li>
<li>freeing an allocated memory region only once;</li>
<li>freeing only allocated memory region;</li>
<li>allocate a particular memory region only once.</li>
</ul>
<p><strong>Sample bugfixes</strong><br /><a href="https://git.kernel.org/cgit/linux/kernel/git/stable/linux-stable.git/commit/?id=665c715" class="external">665c715</a><br /><a href="https://git.kernel.org/cgit/linux/kernel/git/stable/linux-stable.git/commit/?id=984814d" class="external">984814d</a></p> Linux Kernel Safety RuleDB - Feature #5356 (New): 207: IRQ registration and deregistrationhttps://forge.ispras.ru/issues/53562014-10-20T08:48:20ZPavel Andrianovandrianov@ispras.ru
Interrupts are registered by the function <em>int request_irq</em>, which takes a number of interruption, and are deregistered by the function <em>free_irq</em>. The rules of correct usage are:
<ul>
<li>request a particular number of interruption only once;</li>
<li>deregister all registered interrupt handlers on module uploading;</li>
<li>deregister only registered handlers and only for this particular module.</li>
</ul>
<p><strong>Sample bugfix</strong><br /><a href="https://git.kernel.org/cgit/linux/kernel/git/stable/linux-stable.git/commit/?id=94f5659cf" class="external">94f5659cf</a></p> Linux Kernel Safety RuleDB - Feature #5355 (New): 205: All allocated socket buffers should be freedhttps://forge.ispras.ru/issues/53552014-10-20T08:35:02ZPavel Andrianovandrianov@ispras.ru
The dynamic allocation of memory is difficult to check. The suggested rule targets to allocation of socket buffers. The correct usage includes:
<ul>
<li>Freeing all socket buffers to avoid a memory leak.</li>
<li>Freeing a socket buffer only once.</li>
<li>Freeing allocated socket buffers.</li>
</ul>
<p>Sample bugfixes:<br /><a href="https://git.kernel.org/cgit/linux/kernel/git/stable/linux-stable.git/commit/?id=a4e0b4c" class="external">a4e0b4c</a><br /><a href="https://git.kernel.org/cgit/linux/kernel/git/stable/linux-stable.git/commit/?id=8ea008e" class="external">8ea008e</a><br /><a href="https://git.kernel.org/cgit/linux/kernel/git/stable/linux-stable.git/commit/?id=0b1511b" class="external">0b1511b</a><br /><a href="https://git.kernel.org/cgit/linux/kernel/git/stable/linux-stable.git/commit/?id=08f7de1" class="external">08f7de1</a></p> Linux Kernel Safety RuleDB - Feature #5354 (New): 200: DMA maps for SCSI commandshttps://forge.ispras.ru/issues/53542014-10-20T08:19:05ZPavel Andrianovandrianov@ispras.ru
<p><strong>Description</strong></p>
DMA map for SCSI command is created by the function <em>int scsi_dma_map(struct scsi_cmnd *)</em> if its first argument is a correct pointer to a structure of SCSI command. A DMA map is destroyed by function <em>int scsi_dma_unmap(struct scsi_cmnd *)</em>. If <em>scsi_dma_map</em> returns zero, the <em>scsi_dma_unmap</em> is not necessary, but is not an error as well. The correct usage includes:
<ul>
<li>unmap only created maps;</li>
<li>create only one map for particular SCSI command;</li>
<li>cancel all created maps before shutdown of the module.</li>
</ul>
<p>Sample bugfixes <a href="https://git.kernel.org/cgit/linux/kernel/git/stable/linux-stable.git/commit/?id=25e8bc0" class="external">25e8bc0</a>, <a href="https://git.kernel.org/cgit/linux/kernel/git/stable/linux-stable.git/commit/?id=e70f61e" class="external">e70f61e</a></p> Linux Driver Verification - Bug #4437 (New): Make clean in cvc3https://forge.ispras.ru/issues/44372013-08-08T07:33:41ZPavel Andrianovandrianov@ispras.ru
<p>'Make clean' in original folder doesn't clean folder ldv-tools/dscv/rcv/backends/blast/cvc3-dev/</p>