Невозможно интегрировать CBMC в системы сборки

Question

Я пытаюсь использовать CBMC (C Bounded Model Checking: https://www.cprover.org/cbmc/) в проектах C с открытым исходным кодом из GitHub. Для целей этого вопроса давайте рассмотрим следующий проект: https://github.com/reubenhwk/radvd

Проблема возникает, когда я компилирую проект с помощью gcc. Я могу получить исполняемый файл, на котором вызов cbmc, как

cbmc radvd

но я получаю следующее сообщение об ошибке:

CBMC version 5.8 64-bit x86_64 linux
failed to open input file radvd`

Причина должна заключаться в том, что я использовал gcc вместо goto-cc (как описано здесь: http://www.cprover.org/cprover-manual/goto-cc.html), поэтому он может не распознать файл. Я также попытался использовать goto-cc, как объяснено в предыдущей ссылке, а в некоторых примерах, например, http://www.cprover.org/goto-cc/examples/nanosat.html. Тем не менее, так как они являются приведенными примерами, кажется, что cbmc легко работает. Когда я делаю тот же процесс с другим проектом, таким как связанный (radvd) и использую goto-cc вместо gcc, я получаю следующее сообщение при запуске make CC=goto-cc команда:

make  all-am
make[1]: Entering directory '/home/stefano/Documents/github/radvd'
  YACC     gram.c
updating gram.h
  CC       libradvd_parser_a-gram.o
/usr/include/stdlib.h:133:1: error: syntax error before 'strtof128'
PARSING ERROR
Makefile:941: recipe for target 'libradvd_parser_a-gram.o' failed
make[1]: *** [libradvd_parser_a-gram.o] Error 1
make[1]: Leaving directory '/home/stefano/Documents/github/radvd'
Makefile:755: recipe for target 'all' failed
make: *** [all] Error 2`

В настоящее время я использую версию 5.8 cbmc на виртуальной машине Linux (Ubuntu 17.10).

У вас есть идеи о том, как заставить это работать?

Спасибо

Answer 1

Проблема возникает, когда я компилирую проект с помощью gcc.

CBMC не работает на двоичном, подобном gcc.

CBMC анализирует специальный формат файла, .goto который производится goto-cc, Файл, по сути, представляет собой обычную программу, но немного перестроен и содержит некоторую дополнительную информацию, помогающую в анализе.

CBMC отказывается работать на двоичном файле, сгенерированном gcc, потому что он распознает, что файл не находится в .goto формат, который ожидает CBMC.

Когда я использую goto-cc вместо gcc, я получаю следующее сообщение...

Как было отмечено в комментариях, это происходит потому, что goto-cc не знает, что делать с __float128 тип, потому что это специфично для GCC.

Как предполагает Nominal Animal, используя make CC="goto-cc '-D__float128=long double'" следует изменить тип на что-то, что распознает goto-cc, но, вероятно, лучше связаться с разработчиками CBMC и спросить, как лучше всего справиться с этим делом.

Кроме того, если вы еще не сталкивались с этим, руководство пользователя CBMC может быть полезным.