Add regression test for size limit check

This adds a regression test to check that the size limit for
arrays is caught and cleanly handled (with appropriate error).

Author: TGWDB

regression/cbmc/array_too_big/test.c

@@ -0,0 +1,13 @@
+#include <assert.h>
+#include <stdint.h>
+#include <stdlib.h>
+
+int main()
+{
+  size_t size;
+  size = SIZE_MAX;
+  uint8_t *ptr = malloc(size);
+  __CPROVER_assume(ptr != NULL);
+  uint8_t *ptr_end = ptr + size;
+  assert(ptr <= ptr_end);
+}

regression/cbmc/array_too_big/test.desc

@@ -0,0 +1,11 @@
+CORE
+test.c
+--pointer-overflow-check --pointer-check
+^EXIT=6$
+^SIGNAL=0$
+^array too large for flattening$
+--
+^VERIFICATION
+--
+This test is to check that arrays that are too large are correctly
+error handled to prevent exceptions in other parts of the code.