3

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

Stargateur
  • 24,473
  • 8
  • 65
  • 91
s.dallapalma
  • 1,225
  • 1
  • 12
  • 35
  • 1
    cmbc needs to be taught the `__float128` type, I think; just like Haskell's `c2hs` [needed to](https://github.com/haskell/c2hs/issues/191). One might try a dirty, dirty hack: `make CC="goto-cc '-D__float128=long double'"` or similar, to hide the type.. – Nominal Animal Apr 24 '18 at 15:52
  • Thank you. It worked for me for that specific error. – s.dallapalma Apr 27 '18 at 17:17
  • 1
    A much better approach, however, would be to contact the CBMC developer, Daniel Kroening, and ask him to add support for, or at least recognize as a datatype, the `__float128` type; it is a GCC extension supported on certain architectures (see the [quadmath library](https://gcc.gnu.org/onlinedocs/libquadmath/) for details). The other option is to modify your system include files, to remove or hide that datatype and interfaces using it. [...] – Nominal Animal Apr 30 '18 at 16:17
  • [...] Personally, I would consider creating a virtual machine or a chroot jail, for working with goto-cc and cbmc. – Nominal Animal Apr 30 '18 at 16:17

0 Answers0