Add commented out code relating to --malloc-may-fail

Also add some explanation for why it’s commented out

Author: hannes-steffenhagen-diffblue

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -726,6 +726,10 @@ int jbmc_parse_optionst::get_goto_program(
 
     goto_modelt &goto_model = dynamic_cast<goto_modelt &>(*goto_model_ptr);
 
+    // if we added the ansi-c library models here this should also call
+    // add_malloc_may_fail_variable_initializations(goto_model);
+    // here
+
     if(cmdline.isset("validate-goto-model"))
     {
       goto_model.validate();

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -26,6 +26,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <jsil/jsil_language.h>
 
+#include <goto-programs/add_malloc_may_fail_variable_initializations.h>
 #include <goto-programs/adjust_float_expressions.h>
 #include <goto-programs/goto_convert_functions.h>
 #include <goto-programs/goto_inline.h>
@@ -814,7 +815,12 @@ bool goto_analyzer_parse_optionst::process_goto_program(
     link_to_library(
       goto_model, ui_message_handler, cprover_cpp_library_factory);
     link_to_library(goto_model, ui_message_handler, cprover_c_library_factory);
-    #endif
+
+    // these are commented out as well because without the library
+    // this initialization code doesn’t make any sense
+    add_malloc_may_fail_variable_initializations(goto_model);
+
+#endif
 
     // remove function pointers
     log.status() << "Removing function pointers and virtual functions"