Merge pull request #4901 from tautschnig/array-of

C front-end: Permit array_of as array initializer

Author: Daniel Kroening

regression/ansi-c/array_initialization5/main.c

@@ -0,0 +1,7 @@
+// array size greater than MAX_FLATTENED_ARRAY_SIZE
+static unsigned char buffer[10000] = {0};
+
+int main()
+{
+  __CPROVER_assert(buffer[0] == 0, "");
+}

regression/ansi-c/array_initialization5/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

src/ansi-c/c_typecheck_initializer.cpp

@@ -37,7 +37,7 @@ void c_typecheck_baset::do_initializer(
                    "any array must have a size");
 
     // we don't allow initialisation with symbols of array type
-    if(result.id()!=ID_array)
+    if(result.id() != ID_array && result.id() != ID_array_of)
     {
       error().source_location = result.source_location();
       error() << "invalid array initializer " << to_string(result)