Add malloc-may-fail option to goto-checker

And append an `assert(false)` property to every `malloc` call.

Author: petr-bauch

regression/cbmc/malloc-may-fail/main.c

@@ -0,0 +1,9 @@
+#include <assert.h>
+#include <stdint.h>
+#include <stdlib.h>
+
+int main()
+{
+  char *p = malloc(100);
+  assert(p);
+}

regression/cbmc/malloc-may-fail/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--malloc-may-fail
+^EXIT=10$
+^SIGNAL=0$
+^\[malloc.malloc_may_fail.\d+\] line \d+ malloc may fail in ALLOCATE\(malloc_size, 0 != 0\): FAILURE$
+^\[main.assertion.\d+\] line \d+ assertion p: SUCCESS$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

src/analyses/goto_check.cpp

@@ -72,6 +72,7 @@ class goto_checkt
     enable_built_in_assertions=_options.get_bool_option("built-in-assertions");
     enable_assumptions=_options.get_bool_option("assumptions");
     error_labels=_options.get_list_option("error-label");
+    enable_malloc_fail = _options.get_bool_option("malloc-may-fail");
   }
 
   typedef goto_functionst::goto_functiont goto_functiont;
@@ -238,6 +239,7 @@ class goto_checkt
   bool enable_assertions;
   bool enable_built_in_assertions;
   bool enable_assumptions;
+  bool enable_malloc_fail;
 
   typedef optionst::value_listt error_labelst;
   error_labelst error_labels;
@@ -1941,6 +1943,21 @@ void goto_checkt::goto_check(
         if(rw_ok_cond.has_value())
           rhs = *rw_ok_cond;
       }
+
+      if(enable_malloc_fail && code_assign.rhs().id() == ID_side_effect)
+      {
+        const auto &rhs_side_effect = to_side_effect_expr(code_assign.rhs());
+        if(rhs_side_effect.get_statement() == ID_allocate)
+        {
+          add_guarded_property(
+            false_exprt{},
+            "malloc may fail",
+            "malloc may fail",
+            i.code.source_location(),
+            code_assign.rhs(),
+            guardt{true_exprt{}, guard_manager});
+        }
+      }
     }
     else if(i.is_function_call())
     {

src/analyses/goto_check.h

@@ -38,7 +38,8 @@ void goto_check(
   "(div-by-zero-check)(enum-range-check)(signed-overflow-check)(unsigned-"     \
   "overflow-check)"                                                            \
   "(pointer-overflow-check)(conversion-check)(undefined-shift-check)"          \
-  "(float-overflow-check)(nan-check)(no-built-in-assertions)"
+  "(float-overflow-check)(nan-check)(no-built-in-assertions)"                  \
+  "(malloc-may-fail)"
 
 // clang-format off
 #define HELP_GOTO_CHECK \
@@ -55,6 +56,7 @@ void goto_check(
   " --nan-check                  check floating-point for NaN\n" \
   " --no-built-in-assertions     ignore assertions in built-in library\n" \
   " --enum-range-check           checks that all enum type expressions have values in the enum range\n" /* NOLINT(whitespace/line_length) */ \
+  " --malloc-may-fail            enable failures for malloc calls" \
 // clang-format on
 
 #define PARSE_OPTIONS_GOTO_CHECK(cmdline, options) \
@@ -70,6 +72,7 @@ void goto_check(
   options.set_option("undefined-shift-check", cmdline.isset("undefined-shift-check")); /* NOLINT(whitespace/line_length) */  \
   options.set_option("float-overflow-check", cmdline.isset("float-overflow-check")); /* NOLINT(whitespace/line_length) */  \
   options.set_option("nan-check", cmdline.isset("nan-check")); \
-  options.set_option("built-in-assertions", !cmdline.isset("no-built-in-assertions")) /* NOLINT(whitespace/line_length) */
+  options.set_option("built-in-assertions", !cmdline.isset("no-built-in-assertions")); /* NOLINT(whitespace/line_length) */ \
+  options.set_option("malloc-may-fail", cmdline.isset("malloc-may-fail"))
 
 #endif // CPROVER_ANALYSES_GOTO_CHECK_H