Description
I'm using goto-cc to generate a GOTO binary for further CBMC verification and I meet parses errors as follows.
doge2@yunchou-office:~/VSAR-CBMC/cbmc-5.7$ ./goto-cc -c -m64 -pipe -std=c++0x -g -Wall -W -D_REENTRANT -DQT_NETWORK_LIB -DQT_CORE_LIB -DQT_SHARED wc.cpp
/usr/lib/gcc/x86_64-linux-gnu/5/include/stddef.h:436:1: error: parse error before `; namespace std {'
/usr/include/x86_64-linux-gnu/c++/5/bits/c++config.h:200:1: error: parse error before `; } namespace std'
/usr/include/c++/5/bits/move.h:48:1: error: parse error before `{ return reinterpret_cast <'
/usr/include/c++/5/bits/move.h:54:1: error: parse error before `} namespace std {'
/usr/include/c++/5/type_traits:46:1: error: parse error before `} namespace std {'
/usr/include/c++/5/type_traits:81:1: error: parse error before `} ; template <'
/usr/include/c++/5/type_traits:84:1: error: parse error before `< _Tp , __v'
/usr/include/c++/5/type_traits:726:1: error: parse error before `; template < typename'
/usr/include/c++/5/type_traits:751:1: error: parse error before `< _Tp & >'
/usr/include/c++/5/type_traits:842:1: error: parse error before `( ) ) >'
/usr/include/c++/5/type_traits:842:1: error: parse error before `( ) ) >'
PARSING ERROR
The environment I use:
goto-cc : the version contained in CBMC 5.7
Ubuntu 16.04
GCC:5.4
GCC can compile the project correctly.
This error seems to arise from C++ system library instead of my project code. I tried to change to gcc-4.7, gcc-3.4, reran goto-cc and got the same error message. I also tried to use the cbmc-systemc branch(https://github.com/peterschrammel/cbmc/tree/systemc). Error message is different but have no essential difference (Error message generated from different tool version is attatched here).
Unsupported C++11 feature(might be template meta-programming) is said to be responsible for this.
Is there any way to make up for this? Thank you.
Yunchou Li