我正在尝试在来自 GitHub 的开源 C 项目上使用 CBMC（C 有界模型检查： https ://www.cprover.org/cbmc/）。对于这个问题，让我们考虑以下项目：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`
我目前在虚拟 Linux 机器（Ubuntu 17.10）上使用 5.8 版的 cbmc。
你知道如何让它工作吗？
谢谢