Add boundary size tests

for the malloc-max-check option.

Author: petr-bauch

regression/cbmc/malloc-too-large-almost/main.c

@@ -0,0 +1,13 @@
+#include <assert.h>
+#include <stdint.h>
+#include <stdlib.h>
+
+int main()
+{
+  size_t pointer_width = sizeof(void *) * 8;
+  size_t object_bits = 8; // by default
+  size_t cbmc_max_alloc_size = (size_t)1 << (pointer_width - object_bits);
+  int *p2 = malloc(cbmc_max_alloc_size - 1); // try to allocate exactly the max
+
+  return 0;
+}

regression/cbmc/malloc-too-large-almost/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--malloc-max-check
+^EXIT=0$
+^SIGNAL=0$
+^\[malloc.max_allocation_check.\d+\] line \d+ malloc_size < 2 \^ \(pointer_width - object_size\) in ALLOCATE\(malloc_size, 0 != 0\): SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc/malloc-too-large-just-about/main.c

@@ -0,0 +1,14 @@
+#include <assert.h>
+#include <stdint.h>
+#include <stdlib.h>
+
+int main()
+{
+  size_t pointer_width = sizeof(void *) * 8;
+  size_t object_bits = 8; // by default
+  size_t cbmc_max_alloc_size = (size_t)1 << (pointer_width - object_bits);
+  // try to allocate the smallest violating amount
+  int *p3 = malloc(cbmc_max_alloc_size);
+
+  return 0;
+}

regression/cbmc/malloc-too-large-just-about/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--malloc-max-check
+^EXIT=10$
+^SIGNAL=0$
+^\[malloc.max_allocation_check.\d+\] line \d+ malloc_size < 2 \^ \(pointer_width - object_size\) in ALLOCATE\(malloc_size, 0 != 0\): FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring