Используйте Frama-c для анализа проекта с помощью инфраструктуры сборки CMake.
Мне нужно использовать плагин для анализа значений frama-c для анализа некоторых проектов. Эти проекты используют инфраструктуру сборки CMake в качестве системы сборки.
Я использовал frama-c для анализа каждого файла отдельно. Таким образом, информация о точке входа будет потеряна. Точнее, frama-c требует точку входа для файлов, которые не содержат "основную" функцию, и поэтому сложно охватить все функции и выбрать лучшую точку входа в пределах одного файла из проекта.
Мой вопрос заключается в том, есть ли способ, с помощью которого мы можем запустить frama-c для всего проекта в целом (не для файла за файлом)?
1 ответ
Frama-C принимает несколько файлов в командной строке. Это будет работать, если конфигурация препроцессора (опция -cpp-extra-argsИспользуется, в частности, для включает в себя) одинаково для всех файлов.
Если вам нужны разные настройки препроцессора для разных файлов, вы должны предварительно обработать каждый файл отдельно (только cpp, не Frama-C), и сохранить каждый результат как .i файл. Затем вы можете одновременно передать все эти предварительно обработанные файлы в Frama-C. Как правило, первая операция может быть сделана путем настройки процесса сборки.