Structhack support is broken

[xbauch]

#include <malloc.h>
#include <assert.h>

struct Foo
{
  int i;
  char data[1];
};

int main()
{
  struct Foo* foo = malloc(sizeof(struct Foo) + sizeof(char)*2);
  assert(foo);
  foo->data[0]='a';
  assert(foo->data[0]=='a'); // always succeeds
  foo->data[1]='b'; // set data[1]
  assert(foo->data[1]=='b'); // check data[1] -- should succeed
  foo->data[2]='c'; // set data[2]
  assert(foo->data[1]=='b'); //check data[1] again (same test, but fails)

  return 0;
}

CBMC version: 5.12 (develop)
Operating system: ubuntu 18.04
Exact command line resulting in the issue: $> cbmc main.c
What behaviour did you expect: all assert succed
What happened instead: the last assert fails

We already have a regression test (cbmc/Pointer_byte_extract5) that expoits the undefined behaviour (originating from SV-COMP), so I guess if we want to keep it around we should fix it properly.

[hannes-steffenhagen-diffblue]

FWIW the C standard only really allows this sort of thing for flexible array members, which can not have a size.

[tautschnig]

I've tagged this "wontfix" for now and will leave it open for documentation purposes: This test works fine when using an array of size zero or leaving the array size unspecified (making it a proper flexible array member).