CBMC parser error on C++ code

[ahcheongL]

Hello, I'm trying to make cbmc to reproduce a crash I found on exiv2 library, but it seems cbmc's parser couldn't handle my c++ code.

It seems cbmc couldn't handle the following source code token:
using __gnu_cxx::__add_unsigned;

I've tried to make cbmc to handle the specific fragment, but each time I change cbmc's source code, it generates another parsing errors... so I report the case here.

exiv2_report.zip

CBMC version: 5.42.0 (cbmc-5.42.0-52-g9892924eb-dirty)
Operating system: Ubuntu 18.04
Exact command line resulting in the issue: cbmc ./driver.cpp -I ./headers -I ./headers/exiv2
What behaviour did you expect:
What happened instead: Parsing error

• Would you let me know the meaning of the return value of Parser::rStatement?

Thanks

[ahcheongL]

The error message is as follows :

parsing errorfile /usr/include/c++/7/bits/locale_facets.tcc line 380: parse error before 'typedef typename __add_unsigned <'
--- begin invariant violation report ---
Invariant check failed
File: /home/cheong/cbmc/src/cpp/parse.cpp:7539 function: rStatement
Condition: false
Reason: Unimplemented
Backtrace:
/home/cheong/cbmc/build/bin/cbmc(print_backtrace(std::ostream&)+0x4d) [0x55e2f22d54b0]
/home/cheong/cbmc/build/bin/cbmc(get_backtraceabi:cxx11+0x45) [0x55e2f22d56b7]
/home/cheong/cbmc/build/bin/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, std::allocator > const&>(std::__cxx11::basic_string<char, std::char_traits, std::allocator > const&, std::__cxx11::basic_string<char, std::char_traits, std::allocator > const&, int, std::__cxx11::basic_string<char, std::char_traits, std::allocator > const&, std::__cxx11::basic_string<char, std::char_traits, std::allocator > const&)+0x4e) [0x55e2f1b1a097]
/home/cheong/cbmc/build/bin/cbmc(+0x8558eb) [0x55e2f1b198eb]
/home/cheong/cbmc/build/bin/cbmc(Parser::rStatement()+0x1079) [0x55e2f1cb1863]
/home/cheong/cbmc/build/bin/cbmc(Parser::rCompoundStatement()+0xeb) [0x55e2f1cb0609]
/home/cheong/cbmc/build/bin/cbmc(Parser::rFunctionBody(cpp_declaratort&)+0x225) [0x55e2f1cb0401]
/home/cheong/cbmc/build/bin/cbmc(Parser::rOtherDeclaration(cpp_declarationt&, cpp_storage_spect&, cpp_member_spect&, typet&)+0x7d3) [0x55e2f1c9c6f7]
/home/cheong/cbmc/build/bin/cbmc(Parser::rDeclaration(cpp_declarationt&)+0x29d) [0x55e2f1c9b671]
/home/cheong/cbmc/build/bin/cbmc(Parser::rTemplateDecl(cpp_declarationt&)+0x133) [0x55e2f1c9a003]
/home/cheong/cbmc/build/bin/cbmc(Parser::rDefinition(cpp_itemt&)+0xb6) [0x55e2f1c98558]
/home/cheong/cbmc/build/bin/cbmc(Parser::rLinkageBody(std::vector<cpp_itemt, std::allocator<cpp_itemt> >&)+0xd2) [0x55e2f1c99d7e]
/home/cheong/cbmc/build/bin/cbmc(Parser::rNamespaceSpec(cpp_namespace_spect&)+0x2ec) [0x55e2f1c99694]
/home/cheong/cbmc/build/bin/cbmc(Parser::rDefinition(cpp_itemt&)+0x190) [0x55e2f1c98632]
/home/cheong/cbmc/build/bin/cbmc(Parser::rProgram(cpp_itemt&)+0x56) [0x55e2f1c983e6]
/home/cheong/cbmc/build/bin/cbmc(Parser::operator()()+0x52) [0x55e2f1cb56ee]
/home/cheong/cbmc/build/bin/cbmc(cpp_parse()+0x40) [0x55e2f1cb57b1]
/home/cheong/cbmc/build/bin/cbmc(cpp_parsert::parse()+0xb9) [0x55e2f1c1dab3]
/home/cheong/cbmc/build/bin/cbmc(cpp_languaget::parse(std::istream&, std::__cxx11::basic_string<char, std::char_traits, std::allocator > const&)+0x175) [0x55e2f1c1b3e7]
/home/cheong/cbmc/build/bin/cbmc(initialize_goto_model(std::vector<std::__cxx11::basic_string<char, std::char_traits, std::allocator >, std::allocator<std::__cxx11::basic_string<char, std::char_traits, std::allocator > > > const&, message_handlert&, optionst const&)+0x638) [0x55e2f1ef532f]
/home/cheong/cbmc/build/bin/cbmc(cbmc_parse_optionst::get_goto_program(goto_modelt&, optionst const&, cmdlinet const&, ui_message_handlert&)+0xca) [0x55e2f1b24bfc]
/home/cheong/cbmc/build/bin/cbmc(cbmc_parse_optionst::doit()+0x859) [0x55e2f1b23089]
/home/cheong/cbmc/build/bin/cbmc(parse_options_baset::main()+0x117) [0x55e2f22fa9cf]
/home/cheong/cbmc/build/bin/cbmc(main+0x55) [0x55e2f1b1963f]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xe7) [0x7f67b6ee3bf7]
/home/cheong/cbmc/build/bin/cbmc(_start+0x2a) [0x55e2f1b1950a]

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

[ahcheongL]

It says that the parsing code is not implemented for the case, but I think I find code that cbmc handles such cases in Parser::rName(irept &name) in parser.cpp.
However, it is returning true (around parser.cpp:3589) which leads to UNIMPLEMENTED macro.
Can you let me know the meaning of the return value of Parser::rName, too?