test for issue #3653

Author: Daniel Kroening

regression/cbmc/Struct_Initialization/flexible_array_member.c

@@ -0,0 +1,12 @@
+#include <assert.h>
+
+struct f { int w; int x[]; };
+
+struct f f = { 4, { 0, 1, 2, 3 } };
+
+int main()
+{
+  assert(sizeof(f)==sizeof(int));
+  assert(f.x[1]==1);
+  return 0; 
+}

regression/cbmc/Struct_Initialization/flexible_array_member.desc

@@ -0,0 +1,10 @@
+KNOWNBUG
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Based on issue #3653.