Re-implement using defines

to avoid modifying stdlib.c in case the user option is not selected.

Author: petr-bauch

src/ansi-c/ansi_c_internal_additions.cpp

@@ -155,12 +155,6 @@ 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"
-    "int " CPROVER_PREFIX "malloc_failure_mode="+
-      std::to_string(config.ansi_c.malloc_failure_mode)+";\n"
-    "int " CPROVER_PREFIX "malloc_failure_mode_return_null="+
-    std::to_string(config.ansi_c.malloc_failure_mode_return_null)+";\n"
-    "int " CPROVER_PREFIX "malloc_failure_mode_assert_then_assume="+
-    std::to_string(config.ansi_c.malloc_failure_mode_assert_then_assume)+";\n"
     CPROVER_PREFIX "size_t " CPROVER_PREFIX "max_malloc_size="+
     std::to_string(1 << (config.ansi_c.pointer_width -
                          config.bv_encoding.object_bits - 1))+";\n"

src/ansi-c/cprover_library.cpp

@@ -27,6 +27,21 @@ static std::string get_cprover_library_text(
   if(config.ansi_c.string_abstraction)
     library_text << "#define " CPROVER_PREFIX "STRING_ABSTRACTION\n";
 
+  if(
+    config.ansi_c.malloc_failure_mode ==
+    config.ansi_c.malloc_failure_mode_return_null)
+  {
+    library_text << "#define " CPROVER_PREFIX
+                    "MALLOC_FAILURE_MODE_RETURN_NULL\n";
+  }
+  if(
+    config.ansi_c.malloc_failure_mode ==
+    config.ansi_c.malloc_failure_mode_assert_then_assume)
+  {
+    library_text << "#define " CPROVER_PREFIX
+                    "MALLOC_FAILURE_MODE_ASSERT_THEN_ASSUME\n";
+  }
+
   // cprover_library.inc may not have been generated when running Doxygen, thus
   // make Doxygen skip this part
   /// \cond
@@ -45,7 +60,7 @@ std::string get_cprover_library_text(
   const struct cprover_library_entryt cprover_library[],
   const std::string &prologue)
 {
-  std::ostringstream library_text(prologue);
+  std::ostringstream library_text{prologue, std::ios_base::ate};
 
   std::size_t count=0;
 

src/ansi-c/library/cprover.h

@@ -16,13 +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 int __CPROVER_malloc_failure_mode;
 extern __CPROVER_size_t __CPROVER_max_malloc_size;
 
-// malloc failure modes
-extern int __CPROVER_malloc_failure_mode_return_null;
-extern int __CPROVER_malloc_failure_mode_assert_then_assume;
-
 void __CPROVER_assume(__CPROVER_bool assumption) __attribute__((__noreturn__));
 void __CPROVER_assert(__CPROVER_bool assertion, const char *description);
 void __CPROVER_precondition(__CPROVER_bool assertion, const char *description);

src/ansi-c/library/stdlib.c

@@ -116,24 +116,17 @@ inline void *malloc(__CPROVER_size_t malloc_size)
   // and __CPROVER_allocate doesn't, but no one cares
   __CPROVER_HIDE:;
 
-    if(
-      __CPROVER_malloc_failure_mode ==
-      __CPROVER_malloc_failure_mode_return_null)
+#ifdef __CPROVER_MALLOC_FAILURE_MODE_RETURN_NULL
+    if(malloc_size > __CPROVER_max_malloc_size)
     {
-      if(malloc_size > __CPROVER_max_malloc_size)
-      {
-        return (void *)0;
-      }
-    }
-    else if(
-      __CPROVER_malloc_failure_mode ==
-      __CPROVER_malloc_failure_mode_assert_then_assume)
-    {
-      __CPROVER_assert(
-        malloc_size <= __CPROVER_max_malloc_size,
-        "max allocation size exceeded");
-      __CPROVER_assume(malloc_size <= __CPROVER_max_malloc_size);
+      return (void *)0;
     }
+#endif
+#ifdef __CPROVER_MALLOC_FAILURE_MODE_ASSERT_THEN_ASSUME
+    __CPROVER_assert(
+      malloc_size <= __CPROVER_max_malloc_size, "max allocation size exceeded");
+    __CPROVER_assume(malloc_size <= __CPROVER_max_malloc_size);
+#endif
 
     void *malloc_res;
     malloc_res = __CPROVER_allocate(malloc_size, 0);

src/cpp/cprover_library.cpp

@@ -23,6 +23,24 @@ static std::string get_cprover_library_text(
   library_text << "#line 1 \"<builtin-library>\"\n"
                << "#undef inline\n";
 
+  if(config.ansi_c.string_abstraction)
+    library_text << "#define " CPROVER_PREFIX "STRING_ABSTRACTION\n";
+
+  if(
+    config.ansi_c.malloc_failure_mode ==
+    config.ansi_c.malloc_failure_mode_return_null)
+  {
+    library_text << "#define " CPROVER_PREFIX
+                    "MALLOC_FAILURE_MODE_RETURN_NULL\n";
+  }
+  if(
+    config.ansi_c.malloc_failure_mode ==
+    config.ansi_c.malloc_failure_mode_assert_then_assume)
+  {
+    library_text << "#define " CPROVER_PREFIX
+                    "MALLOC_FAILURE_MODE_ASSERT_THEN_ASSUME\n";
+  }
+
   // cprover_library.inc may not have been generated when running Doxygen, thus
   // make Doxygen skip this part
   /// \cond