Linux Driver Verification

Ошибка в функции 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 не помогает - все равно покрытие оказывается слишком велико.