Added malloc failure model to goto-analyzer

Author: Enrico Steffinlongo

src/ansi-c/goto_check_c.h

@@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_ANSI_C_GOTO_CHECK_C_H
 
 #include <goto-programs/goto_functions.h>
+#include <util/config.h>
 
 class goto_modelt;
 class namespacet;
@@ -50,7 +51,8 @@ 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