I'm trying to use CBMC (C Bounded Model Checking: https://www.cprover.org/cbmc/) on open-source C projects from GitHub. For the purpose of this question, let's consider the following project: https://github.com/reubenhwk/radvd
The problem arises when I compile the project with gcc. I'm able to obtain the executable file on which call cbmc like
cbmc radvd
but I obtain the following error message:
CBMC version 5.8 64-bit x86_64 linux
failed to open input file radvd`
The reason should be the fact that I used gcc instead of goto-cc (as explained here: http://www.cprover.org/cprover-manual/goto-cc.html), so might it's unable to recognize the file.
I also tried to use goto-cc as explained in the previous link and in some example like http://www.cprover.org/goto-cc/examples/nanosat.html. However, since they are guided examples it seems to be easy to make cbmc work. When I do the same process with other project, like the linked one (radvd) and use goto-cc instead of gcc I obtain the following message when running make CC=goto-cc command:
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`
I'm currently using the version 5.8 of cbmc on a virtual Linux machine (Ubuntu 17.10).
Do you have any idea on how make it work?
Thank you