Invariant violation with --dump-c

[zhassan-aws]

This issue is derived from model-checking/kani#1722.

Running this sequence of commands:

goto-cc test.c
goto-instrument --add-library a.out b.out
goto-instrument --dump-c b.out

on the following program:

#include <stdlib.h>

int main() {
    calloc(10, 1);
}

results in an invariant violation:

$ goto-instrument --dump-c b.out 
Reading GOTO program from 'b.out'
--- begin invariant violation report ---
Invariant check failed
File: ../src/goto-instrument/dump_c.cpp:118 function: operator()
Condition: symbol.is_type
Reason: Precondition
Backtrace:
goto-instrument(print_backtrace(std::ostream&)+0x50) [0x55b9b39d26a0]
goto-instrument(get_backtrace[abi:cxx11]()+0x169) [0x55b9b39d2c49]
goto-instrument(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) [0x55b9b3297118]
goto-instrument(dump_ct::operator()(std::ostream&)+0x2412) [0x55b9b33ee442]
goto-instrument(dump_c(goto_functionst const&, bool, bool, bool, namespacet const&, std::ostream&)+0x4ea) [0x55b9b33eed0a]
goto-instrument(goto_instrument_parse_optionst::doit()+0x1f18) [0x55b9b32a0258]
goto-instrument(parse_options_baset::main()+0x8f) [0x55b9b329535f]
goto-instrument(main+0x2af) [0x55b9b328600f]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xf3) [0x7f87f52140b3]
goto-instrument(_start+0x2e) [0x55b9b3296b2e]


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

CBMC version: 5.66.0
Operating system: Ubuntu 20.04
Exact command line resulting in the issue:
What behaviour did you expect:
What happened instead:

[tautschnig]

Dump-C's code was written with the assumption that all struct/union types have tags, but this is not actually an invariant of GOTO programs. I'm working on a fix for dump-c.