CBMC unable to verify C++ Hello World - PARSING ERROR

[FlorianBarrau]

CBMC version: 5.28.0

Operating system: Ubuntu 18.04

Exact command line resulting in the issue:
cbmc --cpp11 -I . main.cpp

What behaviour did you expect:
VERIFICATION TRUE, or CBMC is able to conclude.

What happened instead:

CBMC version 5.28.0 (cbmc-5.28.0) 64-bit x86_64 linux
Parsing main.cpp
file /usr/include/c++/7/type_traits line 74: parse error before 'constexpr operator value_type ('
file /usr/include/c++/7/type_traits line 81: parse error before '} ; template <'
file /usr/include/c++/7/type_traits line 2022: parse error before 'struct __attribute__ ( ('
file /usr/include/c++/7/type_traits line 2024: parse error before '} ; template <'
file /usr/include/c++/7/type_traits line 2043: parse error before 'struct __attribute__ ( ('
file /usr/include/c++/7/type_traits line 2045: parse error before '} ; template <'
file /usr/include/c++/7/type_traits line 2808: parse error before '} ) > {'
file /usr/include/c++/7/type_traits line 3109: parse error before '} namespace std __attribute__'
file /usr/include/c++/7/bits/move.h line 74: parse error before '} template < typename'
file /usr/include/c++/7/bits/move.h line 88: parse error before 'return static_cast < _Tp'
PARSING ERROR

C++ Code to reproduce the problem

#include <iostream>

int main() {
    std::cout << "Hello World!";
    return 0;
}

Extra information

1. cbmc -I . main.cpp produce a crash, if we don't specify C++11

CBMC version 5.28.0 (cbmc-5.28.0) 64-bit x86_64 linux
Parsing main.cpp
--- begin invariant violation report ---
Invariant check failed
File: ../src/cpp/parse.cpp:7518 function: rStatement
Condition: false
Reason: Unimplemented
Backtrace:
cbmc(print_backtrace(std::ostream&)+0x4e) [0x556eaffdfe9e]
cbmc(get_backtrace[abi:cxx11]()+0x16a) [0x556eaffe0e2a]
cbmc(std::enable_if<std::is_base_of<invariant_failedt, invariant_failedt>::value, void>::type invariant_violated_structured<invariant_failedt, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&>(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, int, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)+0x4f) [0x556eaf8ab46f]
cbmc(Parser::rStatement()+0xf78) [0x556eaf9ebb58]
cbmc(Parser::rCompoundStatement()+0x15b) [0x556eaf9ebddb]
cbmc(Parser::rFunctionBody(cpp_declaratort&)+0x6c) [0x556eaf9ebf8c]
cbmc(Parser::rOtherDeclaration(cpp_declarationt&, cpp_storage_spect&, cpp_member_spect&, typet&)+0x6b4) [0x556eaf9ec8a4]
cbmc(Parser::rDeclaration(cpp_declarationt&)+0x226) [0x556eaf9ecc76]
cbmc(Parser::rTemplateDecl(cpp_declarationt&)+0x149) [0x556eafa00c69]
cbmc(Parser::rLinkageBody(std::vector<cpp_itemt, std::allocator<cpp_itemt> >&)+0x12f) [0x556eafa01d0f]
cbmc(Parser::rNamespaceSpec(cpp_namespace_spect&)+0x235) [0x556eafa02325]
cbmc(Parser::rProgram(cpp_itemt&)+0x43) [0x556eafa01823]
cbmc(Parser::operator()()+0xaf) [0x556eafa019bf]
cbmc(cpp_parse()+0x9c) [0x556eafa01b8c]
cbmc(cpp_parsert::parse()+0x18f) [0x556eaf96d7df]
cbmc(cpp_languaget::parse(std::istream&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)+0x777) [0x556eaf96bfc7]
cbmc(initialize_goto_model(std::vector<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, std::allocator<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > > > const&, message_handlert&, optionst const&)+0x905) [0x556eafc17075]
cbmc(cbmc_parse_optionst::get_goto_program(goto_modelt&, optionst const&, cmdlinet const&, ui_message_handlert&)+0x1f3) [0x556eaf8ad5a3]
cbmc(cbmc_parse_optionst::doit()+0x4e2) [0x556eaf8b1f22]
cbmc(parse_options_baset::main()+0xa8) [0x556eaf8a9498]
cbmc(main+0x34) [0x556eaf897ed4]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xe7) [0x7f956a43abf7]
cbmc(_start+0x2a) [0x556eaf8aafda]


--- end invariant violation report ---
Aborted (core dumped)

2. I have tried with cbmc 5.15 (default installation when running apt install cbmc) the same problem occur.
3. The same problem occur on my regular code which is not a hello world.

[tautschnig]

Thank you for raising this. We are aware of the C++ front-end needing work, partly documented via https://github.com/diffblue/cbmc/blob/develop/regression/cpp/type_traits_essentials1/test.desc.