Warn when --malloc-may-fail has no effect

f7958df documented that malloc-may-fail needs to be used whenever the
library is added, but users might not actually have had a chance to read
updated documentation. Print a warning at runtime to make it more likely
that users become aware.

Author: tautschnig

regression/contracts/malloc-may-fail-warning/main.c

@@ -0,0 +1,7 @@
+#include <stdlib.h>
+
+void main()
+{
+  int *p = malloc(sizeof(int));
+  __CPROVER_assert(p != NULL, "malloc-may-fail is not set");
+}

regression/contracts/malloc-may-fail-warning/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--add-library _ --malloc-may-fail
+^malloc-may-fail has no effect when an implementation of malloc is already provided$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This test is to confirm that ineffective use of malloc-may-fail yields a
+warning.

regression/contracts/malloc-may-fail-warning/with-malloc.c

@@ -0,0 +1,10 @@
+void *malloc(__CPROVER_size_t size)
+{
+  return __CPROVER_allocate(size, 0);
+}
+
+void main()
+{
+  int *p = malloc(sizeof(int));
+  __CPROVER_assert(p != NULL, "malloc-may-fail is not set");
+}

regression/contracts/malloc-may-fail-warning/with-malloc.desc

@@ -0,0 +1,11 @@
+CORE
+with-malloc.desc
+--malloc-may-fail
+^malloc-may-fail has no effect when an implementation of malloc is already provided$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This test is to confirm that ineffective use of malloc-may-fail yields a
+warning.

src/cbmc/cbmc_parse_options.cpp

@@ -812,6 +812,18 @@ int cbmc_parse_optionst::get_goto_program(
     return CPROVER_EXIT_SUCCESS;
   }
 
+  if(cmdline.isset("malloc-may-fail"))
+  {
+    auto malloc_entry = goto_model.goto_functions.function_map.find("malloc");
+    if(
+      malloc_entry != goto_model.goto_functions.function_map.end() &&
+      malloc_entry->second.body_available())
+    {
+      log.warning() << "malloc-may-fail has no effect when an implementation "
+                    << "of malloc is already provided" << messaget::eom;
+    }
+  }
+
   if(cbmc_parse_optionst::process_goto_program(goto_model, options, log))
     return CPROVER_EXIT_INTERNAL_ERROR;
 

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1066,6 +1066,18 @@ void goto_instrument_parse_optionst::instrument_goto_program()
 
   // we add the library in some cases, as some analyses benefit
 
+  if(cmdline.isset("malloc-may-fail"))
+  {
+    auto malloc_entry = goto_model.goto_functions.function_map.find("malloc");
+    if(
+      malloc_entry != goto_model.goto_functions.function_map.end() &&
+      malloc_entry->second.body_available())
+    {
+      log.warning() << "malloc-may-fail has no effect when an implementation "
+                    << "of malloc is already provided" << messaget::eom;
+    }
+  }
+
   if(cmdline.isset("add-library") ||
      cmdline.isset("mm"))
   {