Merge pull request #6662 from tautschnig/bugfixes/5093-gen-nondet

C nondet symbol factory: arrays may have zero size

Author: tautschnig

regression/cbmc/pointer-to-struct-with-flexible-array-member-as-parameter-to-entry-point/test.desc

@@ -1,10 +1,9 @@
-KNOWNBUG
+CORE
 main.c
 --function testFunc
---
 ^EXIT=0$
 ^SIGNAL=0$
 --
-^EXIT=134$
 --
-Github issue #5093: Pointer to struct with flexible array member as parameter to entry point causes invariant violation
+Github issue #5093: Pointer to struct with flexible array member as parameter to
+entry point causes invariant violation

src/ansi-c/c_nondet_symbol_factory.cpp

@@ -172,9 +172,11 @@ void symbol_factoryt::gen_nondet_array_init(
   auto const &array_type = to_array_type(expr.type());
   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)
+  auto const array_size = numeric_cast<mp_integer>(to_constant_expr(size));
+  DATA_INVARIANT(
+    array_size.has_value() && *array_size >= 0,
+    "Arrays should have positive size");
+  for(mp_integer index = 0; index < *array_size; ++index)
   {
     gen_nondet_init(
       assignments,