Avoid out-of-memory conditions when zero-initializing objects

When code requests large arrays, we should not instantiate them, and
instead use ARRAY_OF.

Fixes: #4602

Author: tautschnig

regression/cbmc-library/calloc-02/main.c

@@ -1,4 +1,5 @@
 #include <assert.h>
+#include <stdint.h>
 #include <stdlib.h>
 
 int main()
@@ -7,6 +8,10 @@ int main()
   if(p)
     assert(p[0] == 0);
 
+  p = calloc(SIZE_MAX, 1);
+  if(p)
+    assert(p[0] == 0);
+
   size_t size;
   size_t num;
   p = calloc(size, num);

regression/cbmc-library/calloc-02/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---unsigned-overflow-check --pointer-check
+--unsigned-overflow-check --pointer-check --arrays-uf-always
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

src/util/expr_initializer.cpp

@@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "arith_tools.h"
 #include "c_types.h"
+#include "magic.h"
 #include "namespace.h"
 #include "pointer_offset_size.h"
 #include "std_code.h"
@@ -133,7 +134,9 @@ optionalt<exprt> expr_initializert<nondet>::expr_initializer_rec(
         return {};
 
       const auto array_size = numeric_cast<mp_integer>(array_type.size());
-      if(array_type.size().id() == ID_infinity || !array_size.has_value())
+      if(
+        array_type.size().id() == ID_infinity || !array_size.has_value() ||
+        *array_size > MAX_FLATTENED_ARRAY_SIZE)
       {
         if(nondet)
           return side_effect_expr_nondett(type, source_location);