GitHub のオープンソース C プロジェクトでCBMC (C Bounded Model Checking: 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`
その理由は、goto-cc の代わりに gcc を使用したため (ここで説明されているように: http://www.cprover.org/cprover-manual/goto-cc.html )、ファイルを認識できない可能性があるためです。また、前のリンクとhttp://www.cprover.org/goto-cc/examples/nanosat.htmlのような例で説明したように、goto-cc を使用しようとしました。ただし、これらはガイド付きの例であるため、cbmc を機能させるのは簡単なようです。リンクされたプロジェクト（radvd）などの他のプロジェクトで同じプロセスを実行し、gcc の代わりに goto-cc を使用すると、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 を使用しています。
それを機能させる方法について何か考えはありますか？
ありがとうございました