Reimplement inside stdlib.c

will be squashed.

Author: petr-bauch

src/ansi-c/ansi_c_internal_additions.cpp

@@ -155,6 +155,10 @@ void ansi_c_internal_additions(std::string &code)
     "void *" CPROVER_PREFIX "allocate("
       CPROVER_PREFIX "size_t size, " CPROVER_PREFIX "bool zero);\n"
     "const void *" CPROVER_PREFIX "alloca_object = 0;\n"
+    CPROVER_PREFIX "size_t " CPROVER_PREFIX "pointer_width="+
+      std::to_string(config.ansi_c.pointer_width)+";\n"
+    CPROVER_PREFIX "size_t " CPROVER_PREFIX "object_bits="+
+      std::to_string(config.bv_encoding.object_bits)+";\n"
 
     // this is ANSI-C
     "extern " CPROVER_PREFIX "thread_local const char __func__["

src/ansi-c/library/cprover.h

@@ -16,6 +16,8 @@ extern const void *__CPROVER_malloc_object;
 extern __CPROVER_size_t __CPROVER_malloc_size;
 extern _Bool __CPROVER_malloc_is_new_array;
 extern const void *__CPROVER_memory_leak;
+extern __CPROVER_size_t __CPROVER_pointer_width;
+extern __CPROVER_size_t __CPROVER_object_bits;
 
 void __CPROVER_assume(__CPROVER_bool assumption) __attribute__((__noreturn__));
 void __CPROVER_assert(__CPROVER_bool assertion, const char *description);

src/ansi-c/library/stdlib.c

@@ -115,6 +115,10 @@ inline void *malloc(__CPROVER_size_t malloc_size)
   // realistically, malloc may return NULL,
   // and __CPROVER_allocate doesn't, but no one cares
   __CPROVER_HIDE:;
+
+  if (malloc_size >= ((__CPROVER_size_t)1 << (__CPROVER_pointer_width - __CPROVER_object_bits)))
+    return (void*)0;
+
   void *malloc_res;
   malloc_res = __CPROVER_allocate(malloc_size, 0);