Add unit test for checking the max malloc size

Ensure that invalid numbers of bits for object id throws, as well as any
overflow if the max allocation size is too big.

Author: Thomas Kiley

unit/Makefile

@@ -14,6 +14,7 @@ SRC += analyses/ai/ai.cpp \
        analyses/does_remove_const/does_expr_lose_const.cpp \
        analyses/does_remove_const/does_type_preserve_const_correctness.cpp \
        analyses/does_remove_const/is_type_at_least_as_const_as.cpp \
+       ansi-c/max_malloc_size.cpp \
        big-int/big-int.cpp \
        compound_block_locations.cpp \
        get_goto_model_from_c_test.cpp \

unit/ansi-c/max_malloc_size.cpp

@@ -0,0 +1,41 @@
+/*******************************************************************\
+
+Module: Unit test for max_malloc_size
+
+Author: Thomas Kiley
+
+\*******************************************************************/
+
+#include <ansi-c/ansi_c_internal_additions.cpp>
+#include <testing-utils/use_catch.h>
+
+TEST_CASE(
+  "max_malloc_size",
+  "[core][ansi-c][ansi_c_internal_additions][max_malloc_size]")
+{
+  cbmc_invariants_should_throwt throw_invariants;
+
+  SECTION("Too many bits for pointer ID")
+  {
+    REQUIRE_THROWS_AS(max_malloc_size(4, 3), invariant_failedt);
+    REQUIRE_THROWS_AS(max_malloc_size(4, 4), invariant_failedt);
+    REQUIRE_THROWS_AS(max_malloc_size(4, 5), invariant_failedt);
+  }
+
+  SECTION("Not enough bits for pointer ID")
+  {
+    REQUIRE_THROWS_AS(max_malloc_size(4, 0), invariant_failedt);
+  }
+
+  SECTION("Max allocation size overflow")
+  {
+    REQUIRE_THROWS_AS(max_malloc_size(128, 63), invariant_failedt);
+  }
+
+  SECTION("Valid allocation size configurations")
+  {
+    // Here we use 4 bits for the object ID, leaving 3 for the offset
+    REQUIRE(max_malloc_size(8, 4) == 8);
+    REQUIRE(max_malloc_size(128, 64) == 9223372036854775808ull /*2^63*/);
+  }
+}

unit/ansi-c/module_dependencies.txt

@@ -0,0 +1,2 @@
+testing-utils
+ansi-c