Stop asserting positive array size

when generating non-deterministic arrays. Zero-sized arrays are (unfortunately)
legal C construct (as for example the regression test shows).

Author: petr-bauch

Diff for: regression/cbmc/Struct_Hack_Initialization/main.c

@@ -0,0 +1,13 @@
+#include <assert.h>
+
+typedef struct stritem
+{
+  unsigned nkey;
+  unsigned cas[];
+} item;
+
+int foo(item *it)
+{
+  assert(it->cas[0] == 0);
+  return 0;
+}

Diff for: regression/cbmc/Struct_Hack_Initialization/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--function foo --bounds-check --pointer-check
+^\[foo.assertion.1\] line \d+ assertion it->cas\[0\] == 0: FAILURE$
+^\[foo.array_bounds.3\] line \d+ array.cas upper bound in it->cas\[\(.*\)0\]: FAILURE$
+^\[foo.array_bounds.2\] line \d+ array.cas dynamic object upper bound in it->cas\[\(.*\)0\]: FAILURE$
+^\[foo.pointer_dereference.2\] line \d+ dereference failure: pointer invalid in it->cas: SUCCESS$
+^\[foo.pointer_dereference.6\] line \d+ dereference failure: pointer outside object bounds in it->cas: FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

Diff for: src/ansi-c/c_nondet_symbol_factory.cpp

@@ -163,7 +163,6 @@ void symbol_factoryt::gen_nondet_array_init(
   const auto &size = array_type.size();
   PRECONDITION(size.id() == ID_constant);
   auto const array_size = numeric_cast_v<size_t>(to_constant_expr(size));
-  DATA_INVARIANT(array_size > 0, "Arrays should have positive size");
   for(size_t index = 0; index < array_size; ++index)
   {
     gen_nondet_init(