Added malloc failure model to goto-analyzer

Author: Enrico Steffinlongo

src/ansi-c/goto_check_c.h

@@ -12,6 +12,8 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_ANSI_C_GOTO_CHECK_C_H
 #define CPROVER_ANSI_C_GOTO_CHECK_C_H
 
+#include <util/config.h>
+
 #include <goto-programs/goto_functions.h>
 
 class goto_modelt;
@@ -50,7 +52,7 @@ void goto_check_c(
   "(assert-to-assume)"                                                         \
   "(no-bounds-check)(no-pointer-check)(no-signed-overflow-check)"              \
   "(no-pointer-primitive-check)(no-undefined-shift-check)"                     \
-  "(no-div-by-zero-check)"
+  "(no-div-by-zero-check)" OPT_CONFIG_LIBRARY
 
 // clang-format off
 #define HELP_GOTO_CHECK \
@@ -125,7 +127,7 @@ void goto_check_c(
   PARSE_OPTION_OVERRIDE(cmdline, options, "div-by-zero-check"); \
   PARSE_OPTION_OVERRIDE(cmdline, options, "signed-overflow-check"); \
   PARSE_OPTION_OVERRIDE(cmdline, options, "undefined-shift-check"); \
-  PARSE_OPTION_OVERRIDE(cmdline, options, "pointer-primitive-check"); \
+  PARSE_OPTION_OVERRIDE(cmdline, options, "pointer-primitive-check");          \
   (void)0
 // clang-format on
 

src/util/config.h

@@ -70,7 +70,8 @@ class symbol_table_baset;
     " {y--no-library} \t disable built-in abstract C library\n"
 
 #define OPT_CONFIG_LIBRARY                                                     \
-  "(malloc-fail-assert)(malloc-fail-null)(malloc-may-fail)(no-malloc-may-fail)"\
+  "(malloc-fail-assert)(malloc-fail-null)(malloc-may-fail)(no-malloc-may-"     \
+  "fail)"                                                                      \
   "(string-abstraction)"
 
 #define HELP_CONFIG_LIBRARY                                                    \