Make --no-standard-checks reinstate old malloc behaviour

The calls to the `set_default_analysis_flags` functions need to be
before the call to `config.set(cmdline)` so that the malloc defaults can
be set before being overridden by any command line specified malloc
behaviour.

src/cbmc/cbmc_parse_options.cpp

@@ -121,10 +121,28 @@ void cbmc_parse_optionst::set_default_analysis_flags(
   // Unwinding assertions required in certain cases for sound verification
   // results. See https://github.com/diffblue/cbmc/issues/6561 for elaboration.
   options.set_option("unwinding-assertions", enabled);
+
+  if(enabled)
+  {
+    config.ansi_c.malloc_may_fail = true;
+    config.ansi_c.malloc_failure_mode =
+      configt::ansi_ct::malloc_failure_modet::malloc_failure_mode_return_null;
+  }
+  else
+  {
+    config.ansi_c.malloc_may_fail = false;
+    config.ansi_c.malloc_failure_mode =
+      configt::ansi_ct::malloc_failure_modet::malloc_failure_mode_none;
+  }
 }
 
 void cbmc_parse_optionst::get_command_line_options(optionst &options)
 {
+  // Enable flags that in combination provide analysis with no surprises
+  // (expected checks and no unsoundness by missing checks).
+  cbmc_parse_optionst::set_default_analysis_flags(
+    options, !cmdline.isset("no-standard-checks"));
+
   if(config.set(cmdline))
   {
     usage_error();
@@ -332,11 +350,6 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
     "self-loops-to-assumptions",
     !cmdline.isset("no-self-loops-to-assumptions"));
 
-  // Enable flags that in combination provide analysis with no surprises
-  // (expected checks and no unsoundness by missing checks).
-  cbmc_parse_optionst::set_default_analysis_flags(
-    options, !cmdline.isset("no-standard-checks"));
-
   // all (other) checks supported by goto_check
   PARSE_OPTIONS_GOTO_CHECK(cmdline, options);
 

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -68,13 +68,29 @@ void goto_analyzer_parse_optionst::set_default_analysis_flags(
   options.set_option("signed-overflow-check", enabled);
   options.set_option("undefined-shift-check", enabled);
 
+  if(enabled)
+  {
+    config.ansi_c.malloc_may_fail = true;
+    config.ansi_c.malloc_failure_mode =
+      configt::ansi_ct::malloc_failure_modet::malloc_failure_mode_return_null;
+  }
+  else
+  {
+    config.ansi_c.malloc_may_fail = false;
+    config.ansi_c.malloc_failure_mode =
+      configt::ansi_ct::malloc_failure_modet::malloc_failure_mode_none;
+  }
+
   // This is in-line with the options we set for CBMC in cbmc_parse_optionst
   // with the exception of unwinding-assertions, which don't make sense in
   // the context of abstract interpretation.
 }
 
 void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
 {
+  goto_analyzer_parse_optionst::set_default_analysis_flags(
+    options, !cmdline.isset("no-standard-checks"));
+
   if(config.set(cmdline))
   {
     usage_error();
@@ -84,9 +100,6 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("function"))
     options.set_option("function", cmdline.get_value("function"));
 
-  goto_analyzer_parse_optionst::set_default_analysis_flags(
-    options, !cmdline.isset("no-standard-checks"));
-
   // all (other) checks supported by goto_check
   PARSE_OPTIONS_GOTO_CHECK(cmdline, options);