Separate collecting function pointer targets [alternative-to: #4536]

jbmc/src/janalyzer/janalyzer_parse_options.cpp

@@ -634,7 +634,7 @@ bool janalyzer_parse_optionst::process_goto_program(const optionst &options)
     goto_partial_inline(goto_model, ui_message_handler);
 
     // remove returns, gcc vectors, complex
-    remove_returns(goto_model);
+    remove_returns(goto_model, log.get_message_handler());
     remove_vector(goto_model);
     remove_complex(goto_model);
 

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -764,7 +764,7 @@ void jbmc_parse_optionst::process_goto_function(
            !model.can_produce_function(id);
   };
 
-  remove_returns(function, function_is_stub);
+  remove_returns(function, log.get_message_handler(), function_is_stub);
 
   replace_java_nondet(function);
 

jbmc/src/jdiff/jdiff_parse_options.cpp

@@ -293,7 +293,7 @@ bool jdiff_parse_optionst::process_goto_program(
     instrument_preconditions(goto_model);
 
     // remove returns, gcc vectors, complex
-    remove_returns(goto_model);
+    remove_returns(goto_model, log.get_message_handler());
     remove_vector(goto_model);
     remove_complex(goto_model);
     rewrite_union(goto_model);

jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp

@@ -154,7 +154,9 @@ void load_and_test_method(
   // Then test both situations.
   THEN("Replace nondet should work after remove returns has been called.")
   {
-    remove_returns(model_function, [](const irep_idt &) { return false; });
+    remove_returns(model_function, null_message_handler, [](const irep_idt &) {
+      return false;
+    });
 
     replace_java_nondet(model_function);
 
@@ -165,7 +167,9 @@ void load_and_test_method(
   {
     replace_java_nondet(model_function);
 
-    remove_returns(model_function, [](const irep_idt &) { return false; });
+    remove_returns(model_function, null_message_handler, [](const irep_idt &) {
+      return false;
+    });
 
     validate_nondet_method_removed(goto_function.body.instructions);
   }
@@ -176,7 +180,9 @@ void load_and_test_method(
     "Replace and convert nondet should work after remove returns has been "
     "called.")
   {
-    remove_returns(model_function, [](const irep_idt &) { return false; });
+    remove_returns(model_function, null_message_handler, [](const irep_idt &) {
+      return false;
+    });
 
     replace_java_nondet(model_function);
 
@@ -193,7 +199,9 @@ void load_and_test_method(
 
     convert_nondet(model_function, null_message_handler, params, ID_java);
 
-    remove_returns(model_function, [](const irep_idt &) { return false; });
+    remove_returns(model_function, null_message_handler, [](const irep_idt &) {
+      return false;
+    });
 
     validate_nondets_converted(goto_function.body.instructions);
   }

src/cbmc/cbmc_parse_options.cpp

@@ -810,7 +810,7 @@ bool cbmc_parse_optionst::process_goto_program(
   instrument_preconditions(goto_model);
 
   // remove returns, gcc vectors, complex
-  remove_returns(goto_model);
+  remove_returns(goto_model, log.get_message_handler());
   remove_vector(goto_model);
   remove_complex(goto_model);
   rewrite_union(goto_model);

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -686,7 +686,7 @@ bool goto_analyzer_parse_optionst::process_goto_program(
     goto_partial_inline(goto_model, ui_message_handler);
 
     // remove returns, gcc vectors, complex
-    remove_returns(goto_model);
+    remove_returns(goto_model, log.get_message_handler());
     remove_vector(goto_model);
     remove_complex(goto_model);
 

src/goto-analyzer/static_simplifier.cpp

@@ -186,7 +186,7 @@ bool static_simplifier(
   }
 
   // restore return types before writing the binary
-  restore_returns(goto_model);
+  restore_returns(goto_model, m.get_message_handler());
   goto_model.goto_functions.update();
 
   m.status() << "Writing goto binary" << messaget::eom;

src/goto-diff/goto_diff_parse_options.cpp

@@ -335,7 +335,7 @@ bool goto_diff_parse_optionst::process_goto_program(
     instrument_preconditions(goto_model);
 
     // remove returns, gcc vectors, complex
-    remove_returns(goto_model);
+    remove_returns(goto_model, log.get_message_handler());
     remove_vector(goto_model);
     remove_complex(goto_model);
     rewrite_union(goto_model);

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -649,7 +649,7 @@ int goto_instrument_parse_optionst::doit()
 
       // restore RETURN instructions in case remove_returns had been
       // applied
-      restore_returns(goto_model);
+      restore_returns(goto_model, log.get_message_handler());
 
       if(cmdline.args.size()==2)
       {
@@ -899,7 +899,7 @@ void goto_instrument_parse_optionst::do_remove_returns()
   remove_returns_done=true;
 
   log.status() << "Removing returns" << messaget::eom;
-  remove_returns(goto_model);
+  remove_returns(goto_model, log.get_message_handler());
 }
 
 void goto_instrument_parse_optionst::get_goto_program()

src/goto-programs/Makefile

@@ -3,6 +3,7 @@ SRC = adjust_float_expressions.cpp \
       class_hierarchy.cpp \
       class_identifier.cpp \
       compute_called_functions.cpp \
+      collect_function_pointer_targets.cpp \
       destructor.cpp \
       destructor_tree.cpp \
       elf_reader.cpp \