Invariant violation when compiling multiple json symbol table files

[zhassan-aws]

CBMC version: 5.30.1
Operating system: Ubuntu 20.04
Exact command line resulting in the issue: symtab2gb getrandom-6f345ac2a566ca4c.json rand_core-f501d635a961dbb4.json --out a.out
What behaviour did you expect: The command to succeed and produce a.out
What happened instead: Invariant check failed:

--- begin invariant violation report ---
Invariant check failed
File: ../src/langapi/mode.cpp:91 function: get_language_from_identifier
Condition: language
Reason: symbol 'tag-std::backtrace::BytesOrWide::951697206286575092-union::Bytes' has unknown mode 'C'
Backtrace:
symtab2gb(print_backtrace(std::ostream&)+0x50) [0x556f951b7d90]
symtab2gb(get_backtrace[abi:cxx11]()+0x169) [0x556f951b8339]
symtab2gb(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&)+0x48) [0x556f951a30a8]
symtab2gb(get_language_from_identifier(namespacet const&, dstringt const&)+0x22f) [0x556f9532e6cf]
symtab2gb(type_to_name[abi:cxx11](namespacet const&, dstringt const&, typet const&)+0x34) [0x556f9532d204]
symtab2gb(linkingt::rename_symbols(std::unordered_set<dstringt, std::hash<dstringt>, std::equal_to<dstringt>, std::allocator<dstringt> > const&)+0x88) [0x556f952fc4c8]
symtab2gb(linkingt::typecheck()+0x10e) [0x556f952fe5de]
symtab2gb(typecheckt::typecheck_main()+0x52) [0x556f95323e32]
symtab2gb(link_goto_model(goto_modelt&, goto_modelt&, message_handlert&)+0x462) [0x556f952a70c2]
symtab2gb(+0x9e03e) [0x556f951a503e]
symtab2gb(symtab2gb_parse_optionst::doit()+0x1b5) [0x556f951a56c5]
symtab2gb(parse_options_baset::main()+0x8f) [0x556f9519f96f]
symtab2gb(main+0x39) [0x556f9519f199]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xf3) [0x7f62c8f760b3]
symtab2gb(_start+0x2e) [0x556f951a2cfe]


--- end invariant violation report ---

Use the following steps to reproduce on the attached tarball:

1. tar xvzf iss470.tar.gz
2. cd iss470
3. symtab2gb getrandom-6f345ac2a566ca4c.json rand_core-f501d635a961dbb4.json --out a.out

The two json files are generated by the Rust Model Checker (RMC) .

Interestingly, running symtab2gb on each of the two json files separately, and then combining them in the goto-cc step works, e.g.:

1. symtab2gb getrandom-6f345ac2a566ca4c.json --out a.out
2. symtab2gb rand_core-f501d635a961dbb4.json --out b.out
3. goto-cc a.out b.out -o c.out
4. cbmc c.out

[tautschnig]

This problem was fixed by #6233.