Description of problem: $ cat foo.cpp #include <iostream> $ cbmc foo.cpp --show-properties --bounds-check --pointer-check CBMC version 5.6 64-bit x86_64 linux Parsing foo.cpp file /usr/include/c++/6.3.1/x86_64-redhat-linux/bits/c++config.h line 2112: parse error before `; } namespace std' file /usr/include/c++/6.3.1/exception line 63: parse error before `) noexcept { }' file /usr/include/c++/6.3.1/exception line 64: parse error before `; virtual const char' file /usr/include/c++/6.3.1/exception line 77: parse error before `) noexcept { }' file /usr/include/c++/6.3.1/exception line 81: parse error before `; virtual const char' file /usr/include/c++/6.3.1/exception line 95: parse error before `; terminate_handler get_terminate (' file /usr/include/c++/6.3.1/exception line 99: parse error before `noexcept ; void terminate' file /usr/include/c++/6.3.1/exception line 104: parse error before `noexcept ; unexpected_handler set_unexpected' file /usr/include/c++/6.3.1/exception line 107: parse error before `noexcept ; unexpected_handler get_unexpected' file /usr/include/c++/6.3.1/exception line 111: parse error before `noexcept ; void unexpected' PARSING ERROR Version-Release number of selected component (if applicable): $ cbmc --version 5.6 How reproducible: every time Steps to Reproduce: 1. echo '#include <iostream>' > foo.cpp 2. cbmc foo.cpp --show-properties --bounds-check --pointer-check 3. Actual results: $ cbmc foo.cpp --show-properties --bounds-check --pointer-check CBMC version 5.6 64-bit x86_64 linux Parsing foo.cpp file /usr/include/c++/6.3.1/x86_64-redhat-linux/bits/c++config.h line 2112: parse error before `; } namespace std' file /usr/include/c++/6.3.1/exception line 63: parse error before `) noexcept { }' file /usr/include/c++/6.3.1/exception line 64: parse error before `; virtual const char' file /usr/include/c++/6.3.1/exception line 77: parse error before `) noexcept { }' file /usr/include/c++/6.3.1/exception line 81: parse error before `; virtual const char' file /usr/include/c++/6.3.1/exception line 95: parse error before `; terminate_handler get_terminate (' file /usr/include/c++/6.3.1/exception line 99: parse error before `noexcept ; void terminate' file /usr/include/c++/6.3.1/exception line 104: parse error before `noexcept ; unexpected_handler set_unexpected' file /usr/include/c++/6.3.1/exception line 107: parse error before `noexcept ; unexpected_handler get_unexpected' file /usr/include/c++/6.3.1/exception line 111: parse error before `noexcept ; void unexpected' PARSING ERROR Expected results: Additional info:
Reported upstream. I regret that this bug is beyond my ability to fix, so we will have to wait for upstream to fix it. In the meantime, if you are able to use cbmc in c++98 mode, that works around the problem.
Macaulay2-1.9.2-1.fc26, Singular-4.1.0p2-1.fc26, arb-2.10.0-1.fc26, cbmc-5.7-1.fc26, coin-or-Cbc-2.9.8-3.fc26, coin-or-Osi-0.107.8-3.fc26, coin-or-SYMPHONY-5.6.14-3.fc26, coin-or-lemon-1.3.1-10.fc26, eclib-20170330-1.fc26, fflas-ffpack-2.2.2-5.fc26, flint-2.5.2-15.fc26, frobby-0.9.0-10.fc26, gap-pkg-float-0.7.5-2.fc26, giac-1.2.3-3.25.fc26, givaro-4.0.2-5.fc26, glpk-4.61-1.fc26, latte-integrale-1.7.3b-3.fc26, libfplll-5.0.3-1.fc26, libgap-4.8.6-1.fc26, linbox-1.4.2-7.fc26, normaliz-3.1.4-1.fc26, ntl-10.3.0-1.fc26, octave-4.2.1-2.fc26, openms-2.1.0-7.20170131gitbde813.fc26, polymake-3.1-2.fc26, pynac-0.7.3-1.fc26, python-cvxopt-1.1.9-4.fc26, sagemath-7.5.1-1.fc26 has been pushed to the Fedora 26 testing repository. If problems still persist, please make note of it in this bug report. See https://fedoraproject.org/wiki/QA:Updates_Testing for instructions on how to install test updates. You can provide feedback for this update here: https://bodhi.fedoraproject.org/updates/FEDORA-2017-4e8cf20cbb
Macaulay2-1.9.2-1.fc26, Singular-4.1.0p2-1.fc26, arb-2.10.0-1.fc26, cbmc-5.7-1.fc26, coin-or-Cbc-2.9.8-3.fc26, coin-or-Osi-0.107.8-3.fc26, coin-or-SYMPHONY-5.6.14-3.fc26, coin-or-lemon-1.3.1-10.fc26, eclib-20170330-1.fc26, fflas-ffpack-2.2.2-5.fc26, flint-2.5.2-15.fc26, frobby-0.9.0-10.fc26, gap-pkg-float-0.7.5-2.fc26, giac-1.2.3-3.25.fc26, givaro-4.0.2-5.fc26, glpk-4.61-1.fc26, latte-integrale-1.7.3b-3.fc26, libfplll-5.0.3-1.fc26, libgap-4.8.6-1.fc26, linbox-1.4.2-7.fc26, normaliz-3.1.4-1.fc26, ntl-10.3.0-1.fc26, octave-4.2.1-2.fc26, openms-2.1.0-7.20170131gitbde813.fc26, polymake-3.1-2.fc26, pynac-0.7.3-1.fc26, python-cvxopt-1.1.9-4.fc26, sagemath-7.5.1-1.fc26 has been pushed to the Fedora 26 stable repository. If problems still persist, please make note of it in this bug report.