CBMC silently omits invalid struct field in GotoC output

[fzaiser]

I discovered this bug working on Kani, in particular the bug model-checking/kani#1243 with @danielsn. Kani there tries to create a struct with a field of type code, which is not allowed in C because a function cannot be stored directly in a struct but has to be behind a pointer. The symbol table correctly records this invalid field type, but the GotoC output (produced with goto-instrument --dump-c) silently omits this invalid field, which confused us for a while when debugging the Kani issue.

CBMC version: 5.60.0
Operating system: macOS 12.3.1
Exact command line resulting in the issue: kani --enable-unstable --gen-c --keep-temps test.rs (I cannot provide a direct example using C code because the issue is about invalid C code only encountered in Kani.)
What behaviour did you expect: CBMC outputs a warning about an invalid struct field or generates some output in test.out.c about the field.
What happened instead: The invalid field is silently omitted in the output.

[tautschnig]

This would have been fixed by #6892 already, just waiting for code reviews.