13.05.2015: Выпущен инструментарий LDV Tools 0.8
Опубликовано Vadim Mutilin в СР, 13/05/2015 - 07:57
Наиболее важные изменения, которые вошли в LDV Tools 0.8:
- Инструмент верификации CPAchecker обновлен до новой версии 1.4 (r14998).
- Инструментарий LDV Tools теперь доступен в виде контейнеров платформы виртуализации Docker, благодаря этому, теперь не требуется установка всех зависимостей на ваш компьютер.
- Улучшения в 13 существующих спецификациях правил:
- Driver becomes not available for unloading permanently.
- Locking a mutex twice or unlocking without prior locking.
- Usage of spin lock and unlock functions.
- Usb alloc/free urb.
- Possible TTY NULL dereference.
- Atomic allocation in interrupt context.
- Memory allocation inside spinlocks.
- NOIO allocation under usb_lock.
- Initialization of completion.
- Error handling in probe().
- All obtained blk requests should be put after all.
- Calling find_next_zero_bit() with arguments in the right order.
- Usb device reference counting with usb_get_dev/usb_put_dev and interface_to_usbdev.
- Добавлены 3 новые спецификации правил:
Результаты валидации инструментария LDV Tools версий 0.8 и 0.7 с различными инструментами верификации на наборе, состоящем из 41 известной ошибки в ядре Linux, представлены ниже в таблице.
| LDV Tools 0.8 | LDV Tools 0.7 | ||||
| BLAST | CPAchecker | BLAST | CPAchecker | ||
| Найденные ошибки | 19 | 18 | 19 | 15 | |
| Пропущенные ошибки | По причине проблем в инструментах верификации | 3 | 2 | 3 | 2 |
| Нехватка памяти (63 гигабайта) | 2 | 0 | 1 | 2 | |
| Нехватка времени (50 минут) | 0 | 5 | 0 | 6 | |
| По другим причинам | 17 | 16 | 18 | 16 | |
Благодаря изменениям, описанным здесь, в инструмент CPAchecker новой версии смог найти на три ошибки больше.
Исходный код LDV Tools 0.8 доступен в репозитории по тегу v0.8. Инструкции по сборке представлены здесь. Если вы хотите использовать собранную версию инструментария LDV Tools, пожалуйста, используйте инструкцию Использование LDV Tools в Docker.