Верификация больших объемов кода

В процессе решения задачи верификации модуля ядра Linux, требующей работы с большим объемом кода, для преодоления ограничений набора инструментов Astraver был разработан набор вспомогательных утилит. Эти утилиты упрощают изучение исходного кода и работу с ним. Страница разработки утилит находится на forge.ispras.ru.

Установка внешних зависимостей утилит осуществляется следующим образом:

cpan cpanm
cpanm --installdeps .

Для удобства работы с программами рекомендуется задать переменные окружения:

Краткое описание функциональности утилит

Каждая из утилит имеет собственную документацию, которая доступна по ключу --help. Ниже представлено краткое описание функциональности и предназначения программ. Программы разбиты на две группы: первая группа используется для трансформации, вторая - для анализа исходного кода.

Трансформация исходного кода

Анализ исходного кода

Данные утилиты предназначены для изучения исходного кода и интерфейсов его взаимодействия с ядром.