CSmith test with random seed 1684847330 has dump-c checksum mismatch

[tautschnig]

https://github.com/diffblue/cbmc/actions/runs/5057664809/jobs/9076711993?pr=6785 reported:

Checksum mismatch: GCC: 0xE09F7B20 dump-c: 0x16014CDF

It seems that the semantics of the original C source as generated by CSmith and the one produced by dump-c differ for the program generated with random seed 1684847330. Needs investigation to figure out whether the bug is in dump-c or goto-program conversion. We need to enable debug output in the test example to see where checksums start diverging.

[tautschnig]

The same issue arises with random seed 1684854437 (https://github.com/diffblue/cbmc/actions/runs/5058960713/jobs/9079812267?pr=7728).

[tautschnig]

The issue once again came up, now with random seed 1697191533 (https://github.com/diffblue/cbmc/actions/runs/6506767120/job/17672954027?pr=7933).

[tautschnig]

Another example is random seed 1707092271.

[tautschnig]

Another example is random seed 1714474363.

[tautschnig]

Another example is random seed 1718809244.

[tautschnig]

Here is a reduce example of the problem:

#include <assert.h>
#include <stdint.h>
struct S0 {
  int32_t f4 : 18;
};
int32_t g_93 = -2;
struct S0 g_164 ;
int32_t g_176 ;
int main () {
  g_176 = (g_164.f4 = g_93);
  assert(g_176 == -2);
}

The code introduced in dbe6455 fails to accurately represent the semantics of the above assignment through a bitfield in the output of dump-c (the GOTO program, however, is correct). Instead, we will need to create local declarations of structs-with-bitfield (or perhaps see whether we have an existing, matching type) to precisely model this.