Dump-C appears incompatible with --dfcc

[tautschnig]

Even when the source code doesn't even have contracts it seems that dynamic frame instrumentation creates some code that convert_compound did not expect:

$ cat simp.c 
#include <assert.h>

int main() {
  int x;
  int y = x;
  assert(y == x);

  return 0;
}
$ goto-cc simp.c -o simp.out
$ goto-instrument --dfcc main --dump-c simp.out 
Reading GOTO program from 'simp.out'
Function Pointer Removal
Virtual function removal
Cleaning inline assembler statements
Trying to force one backedge per target
Loading CPROVER C library (x86_64)
Adding the cprover_contracts library (x86_64)
file <builtin-library-malloc> line 6: symbol '__CPROVER_malloc_is_new_array' already has an initial value
symbol '__CPROVER_alloca_object' already has an initial value
symbol '__CPROVER_new_object' already has an initial value
file <builtin-library-free> line 11: symbol '__CPROVER_malloc_is_new_array' already has an initial value
Instrumenting harness function 'main'
Instrumenting 'malloc'
Instrumenting 'free'
Specializing cprover_contracts functions for assigns clauses of at most 0 targets
Removing unused functions
Updating init function
Setting entry point to main
--- begin invariant violation report ---
Invariant check failed
File: ../src/goto-instrument/dump_c.cpp:630 function: convert_compound
Condition: false
Reason: Unreachable
Backtrace:
goto-instrument(+0x8e6052) [0x5fd8b4449052]
goto-instrument(+0x8e6dcd) [0x5fd8b4449dcd]
goto-instrument(+0x122722) [0x5fd8b3c85722]
goto-instrument(+0x2d0cc6) [0x5fd8b3e33cc6]
goto-instrument(+0x2cfa6b) [0x5fd8b3e32a6b]
goto-instrument(+0x2d6631) [0x5fd8b3e39631]
goto-instrument(+0x2d70af) [0x5fd8b3e3a0af]
goto-instrument(+0x12d8ba) [0x5fd8b3c908ba]
goto-instrument(+0x1204af) [0x5fd8b3c834af]
goto-instrument(+0x110e76) [0x5fd8b3c73e76]
/lib/x86_64-linux-gnu/libc.so.6(+0x29d90) [0x717ca6229d90]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x80) [0x717ca6229e40]
goto-instrument(+0x121d15) [0x5fd8b3c84d15]


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

[remi-delmas-3000]

That's surprising, the instrumentation itself only uses scalar types.