Unexpected verification result about nested struct initialization

[muchang]

#include <assert.h>

typedef int T[];

struct f { int w; T x; };

static struct f f = { 4, { 0, 1, 2, 3 } };

int main()
{
  int i;
  for (i = 0; i < f.w; ++i)
  {
     if (f.x[i] != i)
        { assert(0);} 
  }
 return 0; 
}

CBMC version: 5.10
Operating system: Ubuntu 18.04
Exact command line resulting in the issue: cbmc <file.c>
What behaviour did you expect: result in SUCCESS (proofed by compiling with gcc and executing)
What happened instead: [main.assertion.1] assertion 0: FAILURE

[kroening]

Many thanks; I've made a PR with a test for this as PR #3695.

[tautschnig]

What behaviour do we actually expect here? Looking at the C standard, this is explicitly called out as invalid (paragraph 21/Example 2 in "6.7.2.1 Structure and union specifiers" in C11). Is the desired bug fix for us to reject this during type checking?

[kroening]

This might be a gcc/clang extension, but the documentation doesn't seem to be clear about that.

[tautschnig]

It seems to work with GCC and MSVC, Clang rejects the program.

[SaswatPadhi]

This appears to be a bug even with the latest (5.36) version.