Как мне проанализировать сложный проект, такой как open62541? - PullRequest
Новая
       29

Как мне проанализировать сложный проект, такой как open62541?

3 голосов
/ 20 апреля 2020

Я студент и в настоящее время пытаюсь проанализировать эталонную реализацию протокола OP C Ua в C с помощью cppcheck и frama- c. Моя цель не в том, чтобы проводить очень специализированное тестирование, а в более общих / базовых c тестах, чтобы увидеть, есть ли некоторые очевидные проблемы с кодом.

Проект можно найти здесь

Я использую виртуальную машину с Ubuntu 19.10 и Frama- C версии 20.0 (Calcium).

Я выполнил следующие шаги: 

git clone https://github.com/open62541/open62541.git
cmake -DCMAKE_EXPORT_COMPILE_COMMANDS=1 /path/to/source
frama-c -json-compilation-database /path/to/compile_commands.json

До сих пор все работает, как ожидалось, и ошибок нет.

Однако сейчас у меня возникают проблемы с пониманием, как продолжить. Нужно ли мне проводить анализ всех файлов отдельно или можно добавить весь проект, как с помощью cppcheck?

Как бы я подошел к этому в целом? Нужно ли мне анализировать все файлы шаг за шагом?

Например, я попытался: 

frama-c -json-compilation-database /path/to/compilation_commands.json -val /path/to/open62541/src/

, что возвращает: 

[kernel] Parsing src (with preprocessing)
gcc: warning: /path/to/open62541/src/: linker input file unused because linking not done
[kernel] User Error: cannot find entry point `main'.
  Please use option `-main' for specifying a valid entry point.
[kernel] Frama-C aborted: invalid user input.

Итак, frama- c требуется точка входа, однако я не знаю, какую точку входа мне нужно указать.

Любая помощь по этому вопросу очень ценится. Я прошу прощения за отсутствие понимания. Это мой первый проект такого рода, и я немного ошеломлен frama- c и сложностью проекта open62541.

1 Ответ

3 голосов
/ 21 апреля 2020

Нужно ли мне проводить анализ всех файлов отдельно или можно добавить весь проект, как с помощью cppcheck?

Frama- C может на самом деле анализировать весь проект в одном go при условии, что несколько файлов не определяют одинаковые символы . См. http://blog.frama-c.com/index.php?post / 2018/01/25 / Аналитические сценарии% 3A-помогает-автоматизировать тематические исследования , параграф «Установка источников и тестирование парсинга»:

Список исходных файлов, передаваемых Frama- C, можно получить из файла compile_commands. json. Однако часто бывает так, что анализируемое программное обеспечение содержит несколько двоичных файлов, каждый из которых требует различного набора источников. База данных компиляции JSON не отображает источники, использованные для создания каждого двоичного файла, поэтому не всегда возможно полностью автоматизировать процесс.

Ключевым моментом в вашем случае является то, что compilation_commands.json инструктирует Frama- C о том, как анализировать каждый файл, но вы все равно должны предоставить файлы, которые вы хотите видеть, проанализировали самостоятельно. С вашей текущей командной строкой Frama- C пытается интерпретировать /path/to/open62541/src/ как файл (и терпит неудачу) и не имеет другого файла для анализа. Вот почему вы получаете сообщение об ошибке User Error: cannot find entry point 'main'.

Таким образом, вы должны указать файлы, которые вы хотите проанализировать в командной строке. Это можно сделать двумя способами:

Я использовал первый подход, но Я предлагаю вам использовать второе, так как frama-c-script очень полезно для начала первого анализа.

После того, как вы выполните этот шаг перечисления, вы столкнетесь по крайней мере еще с тремя проблемами:

  • Frama- C будет подавлен # include <sys/param.h>, поскольку этот файл отсутствует в стандартной библиотеке C, поставляемой в комплекте с Frama- C. Либо удалите это включение в исходных файлах, либо добавьте пустые sys/param.h где-нибудь
  • некоторые .c файлы, ссылающиеся на сгенерированные заголовки, которых нет в репозитории git из open62541. Поэтому вам нужно будет скомпилировать репозиторий, чтобы получить эти заголовки перед запуском Frama- C.
  • Frama- C также захлебнется определением макроса UA_STATIC_ASSERT в architecture_definitions.h. Я не исследовал, было ли принято одно из определений, и просто определил его для пустого макроса.

После всего этого у вас должно получиться go.

...