AstraVer Toolset » Deductive Verification Tools for Linux Kernel » Verification Tool Supports

Ошибка возникает потому, что зависимость на get_cred возникает в ядровом коде. Соответственно, декларация get_cred берётся из кода ядра. Если бы зависимость на get_cred возникала в коде модуля, тогда тогда бы спецификация взялась из него. Так как get_cred в коде модуля вообще не вызывается, то в граф модуля она не попадает.

Основная причина в том, что граф строится постепенно. На первой стадии строется граф только по зависимотям ядерной части и сохраняется в кэш первого уровня. Затем строится граф достраивается по зависимостям модуля и сохраняется в кэш второго уровня. Можно перемешать эти два процесса. Это решит проблему. В таком случае не будет разделения кешей на уровни. Оно было нужно для убыстрения работы программы, если изменения не вносятся в заголовочные файлы ядра. Впринципе, программа и так работает довольно быстро и разделение кешей на уровни не имеет особого смысла.

Проблему можно решить иначе. У Dismember есть плагин SmartLib:
Plugin::SmartLib - плагин для избирательного включения спецификаций на декларации функций из файла библиотеки в выводимые данные
Плагин считывает файл file. Парсит декларации функций в нём и спецификации к ним. Если в выводимых данных присутствуют вызовы одной из декларируемых в файле file функций, то эта декларация включается в выводимые данные вместе со своей спецификацией.

В конфигурацию можно добавить строки:
plugin=smartlib
plugin-smartlib-file=/home/work/workspace/work/astraver-spec/parsec/spec_lib.h

Тогда спецификация будет включаться.

У SmartLib есть один недостаток: в своей работе он не может учитывать зависимости по спецификациям.

Поправлено за счёт разрешения таких вхождений.

+ module_declaration -> kernel_macro;
+ module_declaration -> kernel_global;
+ module_declaration -> kernel_function;

Упрощает кэш первого уровня. Теперь в нем лежит только индекс объектов из ядерного кода. Это каим-то образом ломает опцию --cache=1, так как некоторые объекты пропадают. Сам баг поправлен, опция --cache=1 пока не работает.