diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp
index 75f535cc141..de2c69a031d 100644
--- a/jbmc/src/janalyzer/janalyzer_parse_options.cpp
+++ b/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);
 
diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp
index 1cd907e239a..e4732ed306e 100644
--- a/jbmc/src/jbmc/jbmc_parse_options.cpp
+++ b/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);
 
diff --git a/jbmc/src/jdiff/jdiff_parse_options.cpp b/jbmc/src/jdiff/jdiff_parse_options.cpp
index 627d324152d..e716ad7fa68 100644
--- a/jbmc/src/jdiff/jdiff_parse_options.cpp
+++ b/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);
diff --git a/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp b/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp
index 872066ded25..920b915afb8 100644
--- a/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp
+++ b/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);
   }
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index c3ba124b029..730e985f433 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/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);
diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp
index 962cbd39dbb..7ce4e3832c0 100644
--- a/src/goto-analyzer/goto_analyzer_parse_options.cpp
+++ b/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);
 
diff --git a/src/goto-analyzer/static_simplifier.cpp b/src/goto-analyzer/static_simplifier.cpp
index 2f6a86658f7..04b3cd2fa0a 100644
--- a/src/goto-analyzer/static_simplifier.cpp
+++ b/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;
diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp
index 2753ec1d1ba..aa383a4e96c 100644
--- a/src/goto-diff/goto_diff_parse_options.cpp
+++ b/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);
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index c21c8935dc6..ca692cc650f 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/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()
diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp
index 3c579f386b1..b88d8409d50 100644
--- a/src/goto-programs/remove_function_pointers.cpp
+++ b/src/goto-programs/remove_function_pointers.cpp
@@ -38,28 +38,63 @@ class remove_function_pointerst
     bool only_resolve_const_fps,
     const goto_functionst &goto_functions);
 
-  void operator()(goto_functionst &goto_functions);
-
+  /// Call the function pointer removal via an operator
+  /// \param goto_functions: functions to modify
+  /// \param target_map: candidate functions
+  void operator()(
+    goto_functionst &goto_functions,
+    const possible_fp_targets_mapt &target_map);
+
+  /// Call the function pointer removal within the \p goto_program
+  /// \param goto_program: program to modify
+  /// \param function_id: identifier of the function pointer to be removed
+  /// \param target_map: candidate functions
   bool remove_function_pointers(
     goto_programt &goto_program,
-    const irep_idt &function_id);
+    const irep_idt &function_id,
+    const possible_fp_targets_mapt &target_map);
 
   // a set of function symbols
   using functionst = remove_const_function_pointerst::functionst;
 
   /// Replace a call to a dynamic function at location
-  /// target in the given goto-program by a case-split
+  /// \p target in the given goto-program by a case-split
   /// over a given set of functions
   /// \param goto_program: The goto program that contains target
   /// \param function_id: Name of function containing the target
   /// \param target: location with function call with function pointer
-  /// \param functions: The set of functions to consider
-  void remove_function_pointer(
+  /// \param functions: the set of functions to consider
+  void remove_function_pointer_non_const(
     goto_programt &goto_program,
     const irep_idt &function_id,
     goto_programt::targett target,
     const functionst &functions);
 
+  /// Go through the whole model and find all potential function the pointer at
+  ///   \p call site may point to
+  /// \param goto_functions: goto functions to search for potential candidates
+  /// \param call_site: the call site of the function pointer under analysis
+  /// \return the set of the potential functions
+  functionst get_function_pointer_targets(
+    const goto_functionst &goto_functions,
+    goto_programt::const_targett &call_site);
+
+  /// Go through a single function body and find all potential function the
+  ///   pointer at \p call site may point to
+  /// \param goto_program: function body to search for potential functions
+  /// \param call_site: the call site of the function pointer under analysis
+  /// \return the set of the potential functions
+  functionst get_function_pointer_targets(
+    const goto_programt &goto_program,
+    goto_programt::const_targett &call_site);
+
+  /// Go through the whole model and find all potential function the pointer at
+  ///   all call sites
+  /// \param goto_functions: goto functions to search for potential candidates
+  /// \return a map from ids to sets of function candidates
+  possible_fp_targets_mapt
+  get_function_pointer_targets(const goto_functionst &goto_functions);
+
 protected:
   messaget log;
   const namespacet ns;
@@ -74,16 +109,57 @@ class remove_function_pointerst
   // --remove-const-function-pointers instead of --remove-function-pointers
   bool only_resolve_const_fps;
 
+  // Internal variables for communication between function pointer collection
+  //   and the call modification.
+  std::map<irep_idt, bool> remove_const_found_functions;
+  std::map<irep_idt, bool> does_remove_const_success;
+  std::map<irep_idt, bool> only_remove_const_function_pointers_called;
+
+  void set_remove_const_found_functions(const irep_idt &id, bool value)
+  {
+    if(remove_const_found_functions.count(id) == 0 || !value)
+      remove_const_found_functions[id] = value;
+  }
+  void set_does_remove_const_success(const irep_idt &id, bool value)
+  {
+    if(does_remove_const_success.count(id) == 0 || value)
+      does_remove_const_success[id] = value;
+  }
+  void
+  set_only_remove_const_function_pointers_called(const irep_idt &id, bool value)
+  {
+    if(only_remove_const_function_pointers_called.count(id) == 0 || !value)
+      only_remove_const_function_pointers_called[id] = value;
+  }
+
+  bool did_remove_const_success(const irep_idt &id) const
+  {
+    CHECK_RETURN(does_remove_const_success.count(id) > 0);
+    return does_remove_const_success.at(id);
+  }
+  bool was_only_remove_const_function_pointers_called(const irep_idt &id) const
+  {
+    CHECK_RETURN(only_remove_const_function_pointers_called.count(id) > 0);
+    return only_remove_const_function_pointers_called.at(id);
+  }
+  bool did_remove_const_found_functions(const irep_idt &id) const
+  {
+    CHECK_RETURN(remove_const_found_functions.count(id) > 0);
+    return remove_const_found_functions.at(id);
+  }
+
   /// Replace a call to a dynamic function at location
   /// target in the given goto-program by determining
   /// functions that have a compatible signature
   /// \param goto_program: The goto program that contains target
   /// \param function_id: Name of function containing the target
   /// \param target: location with function call with function pointer
-  void remove_function_pointer(
+  /// \param functions: the set of functions to consider
+  void remove_function_pointer_const(
     goto_programt &goto_program,
     const irep_idt &function_id,
-    goto_programt::targett target);
+    goto_programt::targett target,
+    const functionst &functions);
 
   std::unordered_set<irep_idt> address_taken;
 
@@ -104,6 +180,59 @@ class remove_function_pointerst
     const irep_idt &in_function_id,
     code_function_callt &function_call,
     goto_programt &dest);
+
+  /// Refine the \p type in case the forward declaration was incomplete
+  /// \param type: the type to be refined
+  /// \param code: the function call code to get the arguments from
+  /// \return the refined call type
+  static code_typet
+  refine_call_type(const typet &type, const code_function_callt &code);
+
+  /// Try to remove the const function pointers
+  /// \param goto_program: the function body to run the const_removal_check on
+  /// \param functions: the list of functions the const removal found
+  /// \param pointer: the pointer to be resolved
+  /// \param callee_id: function id
+  void try_remove_const_fp(
+    const goto_programt &goto_program,
+    functionst &functions,
+    const exprt &pointer,
+    const irep_idt &callee_id);
+
+  /// From *fp() build the following sequence of instructions:
+  ///
+  /// if (fp=&f1) then goto loc1
+  /// if (fp=&f2) then goto loc2
+  /// ..
+  /// if (fp=&fn) then goto locN
+  /// loc1:  f1(); goto N+1;
+  /// loc2:  f2(); goto N+1;
+  /// ..
+  /// locN:  fn(); goto N+1;
+  /// locN+1:
+  ///
+  /// \param functions: set of function candidates
+  /// \param code: the original function call
+  /// \param function_id: name of the function
+  /// \param target: iterator to the target call-site
+  /// \return the GOTO program for the new code
+  goto_programt build_new_code(
+    const functionst &functions,
+    const code_function_callt &code,
+    const irep_idt &function_id,
+    goto_programt::targett target);
+
+  /// Log the statistics collected during this analysis
+  /// \param target: iterator to the target call-site
+  /// \param functions: the set of function candidates
+  void remove_function_pointer_log(
+    goto_programt::targett target,
+    const functionst &functions) const;
+
+  /// Extract function name from \p called_functions
+  /// \param called_function: the function call expression
+  /// \return function identifier
+  irep_idt get_callee_id(const exprt &called_function) const;
 };
 
 remove_function_pointerst::remove_function_pointerst(
@@ -263,179 +392,158 @@ void remove_function_pointerst::fix_return_type(
     code_assignt(old_lhs, typecast_exprt(tmp_symbol_expr, old_lhs.type()))));
 }
 
-void remove_function_pointerst::remove_function_pointer(
-  goto_programt &goto_program,
-  const irep_idt &function_id,
-  goto_programt::targett target)
+code_typet remove_function_pointerst::refine_call_type(
+  const typet &type,
+  const code_function_callt &code)
 {
-  const code_function_callt &code = target->get_function_call();
+  PRECONDITION(can_cast_type<code_typet>(type));
+  code_typet call_type = to_code_type(type);
 
-  const auto &function = to_dereference_expr(code.function());
-
-  // this better have the right type
-  code_typet call_type=to_code_type(function.type());
-
-  // refine the type in case the forward declaration was incomplete
-  if(call_type.has_ellipsis() &&
-     call_type.parameters().empty())
+  if(call_type.has_ellipsis() && call_type.parameters().empty())
   {
     call_type.remove_ellipsis();
-    forall_expr(it, code.arguments())
-      call_type.parameters().push_back(
-        code_typet::parametert(it->type()));
+    for(const auto &argument : code.arguments())
+      call_type.parameters().push_back(code_typet::parametert{argument.type()});
   }
+  return call_type;
+}
 
-  bool found_functions;
+void remove_function_pointerst::try_remove_const_fp(
+  const goto_programt &goto_program,
+  functionst &functions,
+  const exprt &pointer,
+  const irep_idt &callee_id)
+{
+  PRECONDITION(functions.empty());
 
-  const exprt &pointer = function.pointer();
-  remove_const_function_pointerst::functionst functions;
   does_remove_constt const_removal_check(goto_program, ns);
   const auto does_remove_const = const_removal_check();
+  set_does_remove_const_success(callee_id, does_remove_const.first);
+
   if(does_remove_const.first)
   {
     log.warning().source_location = does_remove_const.second;
     log.warning() << "cast from const to non-const pointer found, "
                   << "only worst case function pointer removal will be done."
                   << messaget::eom;
-    found_functions=false;
+    set_remove_const_found_functions(callee_id, false);
   }
   else
   {
     remove_const_function_pointerst fpr(
       log.get_message_handler(), ns, symbol_table);
 
-    found_functions=fpr(pointer, functions);
-
-    // if found_functions is false, functions should be empty
+    // if remove_const_function fails, functions should be empty
     // however, it is possible for found_functions to be true and functions
     // to be empty (this happens if the pointer can only resolve to the null
     // pointer)
-    CHECK_RETURN(found_functions || functions.empty());
-
-    if(functions.size()==1)
-    {
-      auto call = target->get_function_call();
-      call.function() = *functions.cbegin();
-      target->set_function_call(call);
-      return;
-    }
+    bool temp = fpr(pointer, functions);
+    set_remove_const_found_functions(callee_id, temp);
+    CHECK_RETURN(temp || functions.empty());
   }
+}
 
-  if(!found_functions)
+remove_function_pointerst::functionst
+remove_function_pointerst::get_function_pointer_targets(
+  const goto_functionst &goto_functions,
+  goto_programt::const_targett &call_site)
+{
+  functionst functions;
+  for(const auto &function_pair : goto_functions.function_map)
   {
-    if(only_resolve_const_fps)
-    {
-      // If this mode is enabled, we only remove function pointers
-      // that we can resolve either to an exact function, or an exact subset
-      // (e.g. a variable index in a constant array).
-      // Since we haven't found functions, we would now resort to
-      // replacing the function pointer with any function with a valid signature
-      // Since we don't want to do that, we abort.
-      return;
-    }
+    const auto &function_body = function_pair.second.body;
+    const auto &candidates =
+      get_function_pointer_targets(function_body, call_site);
+    functions.insert(candidates.begin(), candidates.end());
+  }
+  return functions;
+}
+
+remove_function_pointerst::functionst
+remove_function_pointerst::get_function_pointer_targets(
+  const goto_programt &goto_program,
+  goto_programt::const_targett &call_site)
+{
+  PRECONDITION(call_site->is_function_call());
+
+  const code_function_callt &code = call_site->get_function_call();
+  const auto &function = to_dereference_expr(code.function());
+  const auto &refined_call_type = refine_call_type(function.type(), code);
 
-    bool return_value_used=code.lhs().is_not_nil();
+  functionst functions;
+  auto callee_id = get_callee_id(function);
+  try_remove_const_fp(goto_program, functions, function.pointer(), callee_id);
 
+  set_only_remove_const_function_pointers_called(
+    callee_id, !did_remove_const_success(callee_id) && functions.size() == 1);
+  if(
+    !was_only_remove_const_function_pointers_called(callee_id) &&
+    !did_remove_const_found_functions(callee_id) && !only_resolve_const_fps)
+  {
     // get all type-compatible functions
     // whose address is ever taken
-    for(const auto &t : type_map)
+    for(const auto &type_pair : type_map)
     {
-      // address taken?
-      if(address_taken.find(t.first)==address_taken.end())
-        continue;
-
-      // type-compatible?
-      if(!is_type_compatible(return_value_used, call_type, t.second))
-        continue;
-
-      if(t.first=="pthread_mutex_cleanup")
-        continue;
-
-      symbol_exprt expr(t.first, t.second);
-      functions.insert(expr);
+      const auto &candidate_function_name = type_pair.first;
+      const auto &candidate_function_type = type_pair.second;
+
+      // only accept as candidate functions such that:
+      // 1. their address was taken
+      // 2. their type is compatible with the call-site-function type
+      // 3. they're not pthread mutex clean-up
+      if(
+        address_taken.find(candidate_function_name) != address_taken.end() &&
+        is_type_compatible(
+          code.lhs().is_not_nil(),
+          refined_call_type,
+          candidate_function_type) &&
+        candidate_function_name != "pthread_mutex_cleanup")
+      {
+        functions.insert(
+          symbol_exprt{candidate_function_name, candidate_function_type});
+      }
     }
   }
-
-  remove_function_pointer(goto_program, function_id, target, functions);
+  return functions;
 }
 
-void remove_function_pointerst::remove_function_pointer(
+void remove_function_pointerst::remove_function_pointer_const(
   goto_programt &goto_program,
   const irep_idt &function_id,
   goto_programt::targett target,
   const functionst &functions)
 {
-  const code_function_callt &code = target->get_function_call();
-
-  const exprt &function = code.function();
-  const exprt &pointer = to_dereference_expr(function).pointer();
-
-  // the final target is a skip
-  goto_programt final_skip;
-
-  goto_programt::targett t_final = final_skip.add(goto_programt::make_skip());
-
-  // build the calls and gotos
-
-  goto_programt new_code_calls;
-  goto_programt new_code_gotos;
-
-  for(const auto &fun : functions)
+  auto callee_id = get_callee_id(target->get_function_call().function());
+  if(was_only_remove_const_function_pointers_called(callee_id))
   {
-    // call function
-    auto new_call = code;
-    new_call.function() = fun;
-
-    // the signature of the function might not match precisely
-    fix_argument_types(new_call);
-
-    goto_programt tmp;
-    fix_return_type(function_id, new_call, tmp);
-
-    auto call = new_code_calls.add(goto_programt::make_function_call(new_call));
-    new_code_calls.destructive_append(tmp);
-
-    // goto final
-    new_code_calls.add(goto_programt::make_goto(t_final, true_exprt()));
-
-    // goto to call
-    const address_of_exprt address_of(fun, pointer_type(fun.type()));
-
-    const auto casted_address =
-      typecast_exprt::conditional_cast(address_of, pointer.type());
-
-    new_code_gotos.add(
-      goto_programt::make_goto(call, equal_exprt(pointer, casted_address)));
+    auto call = target->get_function_call();
+    call.function() = *functions.cbegin();
+    target->set_function_call(call);
   }
-
-  // fall-through
-  if(add_safety_assertion)
+  else if(
+    did_remove_const_found_functions(callee_id) || !only_resolve_const_fps)
   {
-    goto_programt::targett t =
-      new_code_gotos.add(goto_programt::make_assertion(false_exprt()));
-    t->source_location.set_property_class("pointer dereference");
-    t->source_location.set_comment("invalid function pointer");
+    // If this mode is enabled, we only remove function pointers
+    // that we can resolve either to an exact function, or an exact subset
+    // (e.g. a variable index in a constant array).
+    // Since we haven't found functions, we would now resort to
+    // replacing the function pointer with any function with a valid signature
+    // Since we don't want to do that, we abort.
+    remove_function_pointer_non_const(
+      goto_program, function_id, target, functions);
   }
-  new_code_gotos.add(goto_programt::make_assumption(false_exprt()));
-
-  goto_programt new_code;
+}
 
-  // patch them all together
-  new_code.destructive_append(new_code_gotos);
-  new_code.destructive_append(new_code_calls);
-  new_code.destructive_append(final_skip);
+void remove_function_pointerst::remove_function_pointer_non_const(
+  goto_programt &goto_program,
+  const irep_idt &function_id,
+  goto_programt::targett target,
+  const functionst &functions)
+{
+  const code_function_callt &code = target->get_function_call();
+  const exprt &function = code.function();
 
-  // set locations
-  Forall_goto_program_instructions(it, new_code)
-  {
-    irep_idt property_class=it->source_location.get_property_class();
-    irep_idt comment=it->source_location.get_comment();
-    it->source_location=target->source_location;
-    if(!property_class.empty())
-      it->source_location.set_property_class(property_class);
-    if(!comment.empty())
-      it->source_location.set_comment(comment);
-  }
+  auto new_code = build_new_code(functions, code, function_id, target);
 
   goto_programt::targett next_target=target;
   next_target++;
@@ -450,32 +558,13 @@ void remove_function_pointerst::remove_function_pointer(
   target->type=OTHER;
 
   // report statistics
-  log.statistics().source_location = target->source_location;
-  log.statistics() << "replacing function pointer by " << functions.size()
-                   << " possible targets" << messaget::eom;
-
-  // list the names of functions when verbosity is at debug level
-  log.conditional_output(
-    log.debug(), [&functions](messaget::mstreamt &mstream) {
-      mstream << "targets: ";
-
-      bool first = true;
-      for(const auto &function : functions)
-      {
-        if(!first)
-          mstream << ", ";
-
-        mstream << function.get_identifier();
-        first = false;
-      }
-
-      mstream << messaget::eom;
-    });
+  remove_function_pointer_log(target, functions);
 }
 
 bool remove_function_pointerst::remove_function_pointers(
   goto_programt &goto_program,
-  const irep_idt &function_id)
+  const irep_idt &function_id,
+  const possible_fp_targets_mapt &target_map)
 {
   bool did_something=false;
 
@@ -483,10 +572,14 @@ bool remove_function_pointerst::remove_function_pointers(
     if(target->is_function_call())
     {
       const code_function_callt &code = target->get_function_call();
+      const auto &callee = code.function();
 
       if(code.function().id()==ID_dereference)
       {
-        remove_function_pointer(goto_program, function_id, target);
+        auto callee_id = get_callee_id(callee);
+        CHECK_RETURN(target_map.count(callee_id) > 0);
+        remove_function_pointer_const(
+          goto_program, function_id, target, target_map.at(callee_id));
         did_something=true;
       }
     }
@@ -497,18 +590,20 @@ bool remove_function_pointerst::remove_function_pointers(
   return did_something;
 }
 
-void remove_function_pointerst::operator()(goto_functionst &functions)
+void remove_function_pointerst::operator()(
+  goto_functionst &functions,
+  const possible_fp_targets_mapt &target_map)
 {
   bool did_something=false;
 
-  for(goto_functionst::function_mapt::iterator f_it=
-      functions.function_map.begin();
-      f_it!=functions.function_map.end();
+  for(goto_functionst::function_mapt::iterator f_it =
+        functions.function_map.begin();
+      f_it != functions.function_map.end();
       f_it++)
   {
     goto_programt &goto_program=f_it->second.body;
 
-    if(remove_function_pointers(goto_program, f_it->first))
+    if(remove_function_pointers(goto_program, f_it->first, target_map))
       did_something=true;
   }
 
@@ -533,7 +628,10 @@ bool remove_function_pointers(
       only_remove_const_fps,
       goto_functions);
 
-  return rfp.remove_function_pointers(goto_program, function_id);
+  return rfp.remove_function_pointers(
+    goto_program,
+    function_id,
+    rfp.get_function_pointer_targets(goto_functions));
 }
 
 void remove_function_pointers(
@@ -551,7 +649,7 @@ void remove_function_pointers(
       only_remove_const_fps,
       goto_functions);
 
-  rfp(goto_functions);
+  rfp(goto_functions, rfp.get_function_pointer_targets(goto_functions));
 }
 
 void remove_function_pointers(message_handlert &_message_handler,
@@ -566,3 +664,197 @@ void remove_function_pointers(message_handlert &_message_handler,
     add_safety_assertion,
     only_remove_const_fps);
 }
+
+void remove_function_pointers(
+  message_handlert &_message_handler,
+  goto_modelt &goto_model,
+  const possible_fp_targets_mapt &target_map,
+  bool add_safety_assertion,
+  bool only_remove_const_fps)
+{
+  remove_function_pointerst rfp(
+    _message_handler,
+    goto_model.symbol_table,
+    add_safety_assertion,
+    only_remove_const_fps,
+    goto_model.goto_functions);
+
+  rfp(goto_model.goto_functions, target_map);
+}
+
+possible_fp_targets_mapt
+remove_function_pointerst::get_function_pointer_targets(
+  const goto_functionst &goto_functions)
+{
+  possible_fp_targets_mapt target_map;
+  for(const auto &function_pair : goto_functions.function_map)
+  {
+    const auto &instructions = function_pair.second.body.instructions;
+    for(auto target = instructions.begin(); target != instructions.end();
+        target++)
+    {
+      if(
+        target->is_function_call() &&
+        target->get_function_call().function().id() == ID_dereference)
+      {
+        const auto &function = target->get_function_call().function();
+        irep_idt callee_id = get_callee_id(function);
+        CHECK_RETURN(!callee_id.empty());
+        if(target_map.count(callee_id) == 0)
+        {
+          target_map.emplace(
+            callee_id, get_function_pointer_targets(goto_functions, target));
+        }
+      }
+    }
+  }
+  return target_map;
+}
+
+possible_fp_targets_mapt get_function_pointer_targets(
+  message_handlert &message_handler,
+  goto_modelt &goto_model)
+{
+  remove_function_pointerst rfp(
+    message_handler,
+    goto_model.symbol_table,
+    false,
+    false,
+    goto_model.goto_functions);
+
+  return rfp.get_function_pointer_targets(goto_model.goto_functions);
+}
+
+goto_programt remove_function_pointerst::build_new_code(
+  const functionst &functions,
+  const code_function_callt &code,
+  const irep_idt &function_id,
+  goto_programt::targett target)
+{
+  // the final target is a skip
+  goto_programt final_skip;
+  const exprt &pointer = to_dereference_expr(code.function()).pointer();
+  goto_programt::targett t_final = final_skip.add(goto_programt::make_skip());
+
+  goto_programt new_code_calls;
+  goto_programt new_code_gotos;
+  for(const auto &function : functions)
+  {
+    // call function
+    auto new_call = code;
+
+    new_call.function() = function;
+
+    // the signature of the function might not match precisely
+    fix_argument_types(new_call);
+
+    goto_programt tmp;
+    fix_return_type(function_id, new_call, tmp);
+
+    auto call = new_code_calls.add(goto_programt::make_function_call(new_call));
+    new_code_calls.destructive_append(tmp);
+
+    // goto final
+    new_code_calls.add(goto_programt::make_goto(t_final, true_exprt{}));
+
+    // goto to call
+    const auto casted_address = typecast_exprt::conditional_cast(
+      address_of_exprt{function, pointer_type(function.type())},
+      pointer.type());
+
+    const auto goto_it = new_code_gotos.add(
+      goto_programt::make_goto(call, equal_exprt{pointer, casted_address}));
+
+    // set locations for the above goto
+    irep_idt property_class = goto_it->source_location.get_property_class();
+    irep_idt comment = goto_it->source_location.get_comment();
+    goto_it->source_location = target->source_location;
+    if(!property_class.empty())
+      goto_it->source_location.set_property_class(property_class);
+    if(!comment.empty())
+      goto_it->source_location.set_comment(comment);
+  }
+
+  // fall-through
+  if(add_safety_assertion)
+  {
+    goto_programt::targett t =
+      new_code_gotos.add(goto_programt::make_assertion(false_exprt{}));
+    t->source_location.set_property_class("pointer dereference");
+    t->source_location.set_comment("invalid function pointer");
+  }
+  new_code_gotos.add(goto_programt::make_assumption(false_exprt{}));
+
+  goto_programt new_code;
+
+  // patch them all together
+  new_code.destructive_append(new_code_gotos);
+  new_code.destructive_append(new_code_calls);
+  new_code.destructive_append(final_skip);
+
+  return new_code;
+}
+
+void remove_function_pointerst::remove_function_pointer_log(
+  goto_programt::targett target,
+  const functionst &functions) const
+{
+  log.statistics().source_location = target->source_location;
+  log.statistics() << "replacing function pointer by " << functions.size()
+                   << " possible targets" << messaget::eom;
+
+  // list the names of functions when verbosity is at debug level
+  log.conditional_output(
+    log.debug(), [&functions](messaget::mstreamt &mstream) {
+      mstream << "targets: ";
+
+      bool first = true;
+      for(const auto &function : functions)
+      {
+        if(!first)
+          mstream << ", ";
+
+        mstream << function.get_identifier();
+        first = false;
+      }
+
+      mstream << messaget::eom;
+    });
+}
+
+irep_idt
+remove_function_pointerst::get_callee_id(const exprt &called_function) const
+{
+  irep_idt callee_id;
+  bool contains_code = false;
+  auto type_contains_code = [&contains_code](const typet &t) {
+    if(t.id() == ID_code)
+      contains_code = true;
+  };
+
+  called_function.visit_post(
+    [&callee_id, &type_contains_code, &contains_code](const exprt &e) {
+      if(e.id() == ID_symbol)
+      {
+        e.type().visit(type_contains_code);
+        if(contains_code)
+        {
+          callee_id = to_symbol_expr(e).get_identifier();
+          return;
+        }
+      }
+      if(e.id() == ID_dereference)
+      {
+        const auto &pointer = to_dereference_expr(e).pointer();
+        if(pointer.id() == ID_symbol)
+          callee_id = to_symbol_expr(pointer).get_identifier();
+        if(pointer.id() == ID_member)
+        {
+          pointer.type().visit(type_contains_code);
+          if(contains_code)
+            callee_id = to_member_expr(pointer).get_component_name();
+        }
+      }
+    });
+  return callee_id;
+}
diff --git a/src/goto-programs/remove_function_pointers.h b/src/goto-programs/remove_function_pointers.h
index bff989e1cea..1b757f04ef6 100644
--- a/src/goto-programs/remove_function_pointers.h
+++ b/src/goto-programs/remove_function_pointers.h
@@ -16,12 +16,28 @@ Date: June 2003
 
 #include <util/irep.h>
 
+#include <map>
+
+#include "remove_const_function_pointers.h"
+
 class goto_functionst;
 class goto_programt;
 class goto_modelt;
 class message_handlert;
 class symbol_tablet;
 
+using possible_fp_targetst = remove_const_function_pointerst::functionst;
+using possible_fp_targets_mapt = std::map<irep_idt, possible_fp_targetst>;
+
+/// Go through the whole model and find all potential function the pointer at
+///   all call sites
+/// \param message_handler: a message handler for reporting
+/// \param goto_model: model to search for potential functions
+/// \return a map from ids to sets of function candidates
+possible_fp_targets_mapt get_function_pointer_targets(
+  message_handlert &message_handler,
+  goto_modelt &goto_model);
+
 // remove indirect function calls
 // and replace by case-split
 void remove_function_pointers(
@@ -30,6 +46,20 @@ void remove_function_pointers(
   bool add_safety_assertion,
   bool only_remove_const_fps=false);
 
+/// Replace all calls to a dynamic function by a case-split over a given set of
+///   candidate functions
+/// \param _message_handler: a message handler for reporting
+/// \param goto_model: model to search for potential functions
+/// \param target_map: candidate functions
+/// \param add_safety_assertion: check that at least one function matches
+/// \param only_remove_const_fps: restrict the pointer remove to const
+void remove_function_pointers(
+  message_handlert &_message_handler,
+  goto_modelt &goto_model,
+  const possible_fp_targets_mapt &target_map,
+  bool add_safety_assertion,
+  bool only_remove_const_fps = false);
+
 void remove_function_pointers(
   message_handlert &_message_handler,
   symbol_tablet &symbol_table,
diff --git a/src/goto-programs/remove_returns.cpp b/src/goto-programs/remove_returns.cpp
index 57d515d4865..3d1d65cca26 100644
--- a/src/goto-programs/remove_returns.cpp
+++ b/src/goto-programs/remove_returns.cpp
@@ -13,11 +13,15 @@ Date:   September 2009
 
 #include "remove_returns.h"
 
+#include <util/c_types.h>
+#include <util/exception_utils.h>
+#include <util/fresh_symbol.h>
 #include <util/std_expr.h>
 #include <util/suffix.h>
 
 #include "goto_model.h"
 
+#include "remove_function_pointers.h"
 #include "remove_skip.h"
 
 #define RETURN_VALUE_SUFFIX "#return_value"
@@ -25,8 +29,10 @@ Date:   September 2009
 class remove_returnst
 {
 public:
-  explicit remove_returnst(symbol_table_baset &_symbol_table):
-    symbol_table(_symbol_table)
+  explicit remove_returnst(
+    symbol_table_baset &_symbol_table,
+    message_handlert &m)
+    : log(m), symbol_table(_symbol_table)
   {
   }
 
@@ -40,8 +46,18 @@ class remove_returnst
   void restore(
     goto_functionst &goto_functions);
 
+  /// Build the internal map to know the potential function pointer targets
+  /// \param goto_model: The model to search for the targets
+  void build_fp_targets(goto_modelt &goto_model)
+  {
+    possible_fp_targets_map =
+      get_function_pointer_targets(log.get_message_handler(), goto_model);
+  }
+
 protected:
+  messaget log;
   symbol_table_baset &symbol_table;
+  possible_fp_targets_mapt possible_fp_targets_map;
 
   void replace_returns(
     const irep_idt &function_id,
@@ -59,6 +75,29 @@ class remove_returnst
 
   optionalt<symbol_exprt>
   get_or_create_return_value_symbol(const irep_idt &function_id);
+
+  /// Remove return of a complete function call
+  /// \param target: the function call instruction iterator
+  /// \param goto_program: the GOTO program to be updated
+  void do_function_call_complete(
+    goto_programt::targett target,
+    goto_programt &goto_program);
+
+  /// Remove return of a complete function call of a function pointer
+  /// \param target: the function call instruction iterator
+  /// \param possible_fp_targets: functions the pointer may point to
+  /// \param goto_program: the GOTO program to be updated
+  void do_function_call_complete(
+    goto_programt::targett target,
+    const possible_fp_targetst &possible_fp_targets,
+    goto_programt &goto_program);
+
+  /// Remove return of a stub function call
+  /// \param target: the function call instruction iterator
+  /// \param goto_program: the GOTO program to be updated
+  void do_function_call_stub(
+    goto_programt::targett target,
+    goto_programt &goto_program);
 };
 
 optionalt<symbol_exprt>
@@ -149,72 +188,59 @@ bool remove_returnst::do_function_calls(
 
   Forall_goto_program_instructions(i_it, goto_program)
   {
-    if(i_it->is_function_call())
-    {
-      code_function_callt function_call = i_it->get_function_call();
+    if(!i_it->is_function_call())
+      continue;
 
-      INVARIANT(
-        function_call.function().id() == ID_symbol,
-        "indirect function calls should have been removed prior to running "
-        "remove-returns");
+    code_function_callt function_call = i_it->get_function_call();
 
-      const irep_idt function_id =
-        to_symbol_expr(function_call.function()).get_identifier();
+    INVARIANT(
+      function_call.function().id() == ID_symbol ||
+        function_call.function().id() == ID_dereference,
+      "only direct function calls (via a symbol) or indirect function calls "
+      "(via a dereference) are supported");
 
-      // Do we return anything?
-      if(
-        to_code_type(function_call.function().type()).return_type() !=
-          empty_typet() &&
-        function_call.lhs().is_not_nil())
-      {
-        // replace "lhs=f(...)" by
-        // "f(...); lhs=f#return_value; DEAD f#return_value;"
-
-        exprt rhs;
-
-        bool is_stub = function_is_stub(function_id);
-        optionalt<symbol_exprt> return_value;
-
-        if(!is_stub)
-        {
-          return_value = get_or_create_return_value_symbol(function_id);
-          CHECK_RETURN(return_value.has_value());
-
-          // The return type in the definition of the function may differ
-          // from the return type in the declaration.  We therefore do a
-          // cast.
-          rhs = typecast_exprt::conditional_cast(
-            *return_value, function_call.lhs().type());
-        }
-        else
-        {
-          rhs = side_effect_expr_nondett(
-            function_call.lhs().type(), i_it->source_location);
-        }
-
-        goto_programt::targett t_a = goto_program.insert_after(
-          i_it,
-          goto_programt::make_assignment(
-            code_assignt(function_call.lhs(), rhs), i_it->source_location));
-
-        // fry the previous assignment
-        function_call.lhs().make_nil();
-
-        if(!is_stub)
-        {
-          goto_program.insert_after(
-            t_a,
-            goto_programt::make_dead(*return_value, i_it->source_location));
-        }
-
-        // update the call
-        i_it->set_function_call(function_call);
-
-        requires_update = true;
-      }
+    bool is_function_pointer = function_call.function().id() == ID_dereference;
+
+    const auto &function_symbol =
+      is_function_pointer
+        ? to_dereference_expr(function_call.function()).pointer()
+        : function_call.function();
+    const auto &function_id = to_symbol_expr(function_symbol).get_identifier();
+
+    // Do we return anything?
+    if(
+      to_code_type(function_call.function().type()).return_type() ==
+        empty_typet() ||
+      !function_call.lhs().is_not_nil())
+      continue;
+
+    if(is_function_pointer)
+    {
+      // f may point to {f1,f2,..}=possible_fp_targets_map[function_id]
+      // lhs=*f(..) => *f(..); lhs = (f == f1 ? f1#return_value : f == f2 ? ..);
+      do_function_call_complete(
+        i_it, possible_fp_targets_map[function_id], goto_program);
+    }
+    else if(function_is_stub(function_id))
+    {
+      // stub:
+      // lhs=f(..) => f(..); lhs=nondet;
+      do_function_call_stub(i_it, goto_program);
+    }
+    else
+    {
+      // lhs=f(..) => f(..); lhs=f#return_value;
+      do_function_call_complete(i_it, goto_program);
     }
-  }
 
+    // fry the previous assignment
+    function_call.lhs().make_nil();
+
+    // update the call
+    i_it->set_function_call(function_call);
+
+    requires_update = true;
+  }
   return requires_update;
 }
 
@@ -257,35 +283,27 @@ void remove_returnst::operator()(
 /// removes returns
 void remove_returns(
   symbol_table_baset &symbol_table,
+  message_handlert &m,
   goto_functionst &goto_functions)
 {
-  remove_returnst rr(symbol_table);
+  remove_returnst rr(symbol_table, m);
   rr(goto_functions);
 }
 
-/// Removes returns from a single function. Only usable with Java programs at
-/// the moment; to use it with other languages, they must annotate their stub
-/// functions with ID_C_incomplete as currently done in
-/// java_bytecode_convert_method.cpp.
-///
-/// This will generate \#return_value variables, if not already present, for
-/// both the function being altered *and* any callees.
-/// \param goto_model_function: function to transform
-/// \param function_is_stub: function that will be used to test whether a given
-///   callee has been or will be given a body. It should return true if so, or
-///   false if the function will remain a bodyless stub.
 void remove_returns(
   goto_model_functiont &goto_model_function,
+  message_handlert &m,
   function_is_stubt function_is_stub)
 {
-  remove_returnst rr(goto_model_function.get_symbol_table());
+  remove_returnst rr(goto_model_function.get_symbol_table(), m);
   rr(goto_model_function, function_is_stub);
 }
 
 /// removes returns
-void remove_returns(goto_modelt &goto_model)
+void remove_returns(goto_modelt &goto_model, message_handlert &m)
 {
-  remove_returnst rr(goto_model.symbol_table);
+  remove_returnst rr(goto_model.symbol_table, m);
+  rr.build_fp_targets(goto_model);
   rr(goto_model.goto_functions);
 }
 
@@ -402,9 +420,9 @@ void remove_returnst::restore(goto_functionst &goto_functions)
 }
 
 /// restores return statements
-void restore_returns(goto_modelt &goto_model)
+void restore_returns(goto_modelt &goto_model, message_handlert &m)
 {
-  remove_returnst rr(goto_model.symbol_table);
+  remove_returnst rr(goto_model.symbol_table, m);
   rr.restore(goto_model.goto_functions);
 }
 
@@ -430,3 +448,141 @@ bool is_return_value_symbol(const symbol_exprt &symbol_expr)
 {
   return is_return_value_identifier(symbol_expr.get_identifier());
 }
+
+void remove_returnst::do_function_call_complete(
+  goto_programt::targett target,
+  goto_programt &goto_program)
+{
+  const auto &function_call = target->get_function_call();
+  const auto &function_id =
+    to_symbol_expr(function_call.function()).get_identifier();
+
+  // The return type in the definition of the function may differ
+  // from the return type in the declaration.  We therefore do a
+  // cast.
+  optionalt<symbol_exprt> return_value =
+    get_or_create_return_value_symbol(function_id);
+  CHECK_RETURN(return_value.has_value());
+
+  // replace "lhs=f(...)" by
+  // "f(...); lhs=f#return_value; DEAD f#return_value;"
+  goto_programt::targett t_a = goto_program.insert_after(
+    target,
+    goto_programt::make_assignment(
+      code_assignt{function_call.lhs(),
+                   typecast_exprt::conditional_cast(
+                     *return_value, function_call.lhs().type())},
+      target->source_location));
+
+  goto_program.insert_after(
+    t_a, goto_programt::make_dead(*return_value, target->source_location));
+}
+
+void remove_returnst::do_function_call_complete(
+  goto_programt::targett target,
+  const possible_fp_targetst &possible_fp_targets,
+  goto_programt &goto_program)
+{
+  PRECONDITION(target->is_function_call());
+  const auto &function_call = target->get_function_call();
+  PRECONDITION(function_call.function().id() == ID_dereference);
+  const auto &function_symbol =
+    to_dereference_expr(function_call.function()).pointer();
+  PRECONDITION(function_symbol.id() == ID_symbol);
+  const auto &function_id = to_symbol_expr(function_symbol).get_identifier();
+  if(possible_fp_targets.empty())
+    throw incorrect_goto_program_exceptiont{
+      "the function pointer " + id2string(function_id) +
+        " does not have any potential targets",
+      target->source_location};
+
+  cond_exprt rhs(exprt::operandst{}, function_call.lhs().type());
+  std::vector<symbol_exprt> return_values;
+
+  const auto &first_target_id = possible_fp_targets.begin()->get_identifier();
+  const auto first_target_symbol = symbol_table.lookup(first_target_id);
+  CHECK_RETURN(first_target_symbol);
+
+  auto &pointer_lhs_symbol = get_fresh_aux_symbol(
+    pointer_type(function_call.lhs().type()),
+    "", // no name prefix
+    "p_lhs",
+    target->source_location,
+    first_target_symbol->mode,
+    symbol_table);
+  symbol_exprt pointer_lhs_expr = pointer_lhs_symbol.symbol_expr();
+
+  exprt::operandst disjunction_operands;
+
+  for(const auto &target_expr : possible_fp_targets)
+  {
+    irep_idt target_id = target_expr.get_identifier();
+    const symbolt *target_symbol = symbol_table.lookup(target_id);
+    CHECK_RETURN(target_symbol);
+
+    // The return type in the definition of the function may differ
+    // from the return type in the declaration.  We therefore do a
+    // cast.
+    optionalt<symbol_exprt> return_value =
+      get_or_create_return_value_symbol(target_id);
+    CHECK_RETURN(return_value.has_value());
+    return_values.push_back(*return_value);
+
+    const auto f_equals_f_i = equal_exprt{
+      function_call.function(), address_of_exprt{target_symbol->symbol_expr()}};
+    disjunction_operands.push_back(f_equals_f_i);
+    rhs.add_case(f_equals_f_i, address_of_exprt{*return_value});
+  }
+
+  // replace "lhs=*f(...)" by
+  //
+  // assert(f==f1 || f==f2 || ..); // so that the user knows
+  // assume(f==f1 || f==f2 || ..); // so that we abort this execution
+  // T* p_lhs = lhs = (f == f1 ? &f1#return_value : f == f2
+  //                           ? &f2#return_value .. );
+  // f*(...);
+  // lhs = *p_lhs;
+  // DEAD f1#return_value;
+  // DEAD f2#return_value;
+  // ..
+  // DEAD p_lhs
+  goto_program.insert_before(
+    target,
+    goto_programt::make_assertion(
+      disjunction(disjunction_operands), target->source_location));
+  goto_program.insert_before(
+    target,
+    goto_programt::make_assumption(
+      disjunction(disjunction_operands), target->source_location));
+  goto_program.insert_before(
+    target,
+    goto_programt::make_assignment(
+      code_assignt{pointer_lhs_expr, rhs}, target->source_location));
+  goto_programt::targett t_a = goto_program.insert_after(
+    target,
+    goto_programt::make_assignment(
+      code_assignt{function_call.lhs(), dereference_exprt{pointer_lhs_expr}},
+      target->source_location));
+
+  for(const auto &return_value : return_values)
+    t_a = goto_program.insert_after(
+      t_a, goto_programt::make_dead(return_value, target->source_location));
+  goto_program.insert_after(
+    t_a, goto_programt::make_dead(pointer_lhs_expr, target->source_location));
+}
+
+void remove_returnst::do_function_call_stub(
+  goto_programt::targett target,
+  goto_programt &goto_program)
+{
+  const auto &function_call = target->get_function_call();
+
+  // replace "lhs=f(...)" by "f(...); lhs=nondet;"
+  goto_program.insert_after(
+    target,
+    goto_programt::make_assignment(
+      code_assignt{function_call.lhs(),
+                   side_effect_expr_nondett{function_call.lhs().type(),
+                                            target->source_location}},
+      target->source_location));
+}
diff --git a/src/goto-programs/remove_returns.h b/src/goto-programs/remove_returns.h
index 5d990f82e60..60c6553dd5e 100644
--- a/src/goto-programs/remove_returns.h
+++ b/src/goto-programs/remove_returns.h
@@ -73,6 +73,7 @@ Date:   September 2009
 
 #include <functional>
 
+#include <util/message.h>
 #include <util/std_types.h>
 
 class goto_functionst;
@@ -82,18 +83,36 @@ class namespacet;
 class symbol_table_baset;
 class symbol_exprt;
 
-void remove_returns(symbol_table_baset &, goto_functionst &);
+void remove_returns(
+  symbol_table_baset &symbol_table,
+  message_handlert &m,
+  goto_functionst &);
 
 typedef std::function<bool(const irep_idt &)> function_is_stubt;
 
-void remove_returns(goto_model_functiont &, function_is_stubt);
-
-void remove_returns(goto_modelt &);
+/// Removes returns from a single function. Only usable with Java programs at
+/// the moment; to use it with other languages, they must annotate their stub
+/// functions with ID_C_incomplete as currently done in
+/// java_bytecode_convert_method.cpp.
+///
+/// This will generate \#return_value variables, if not already present, for
+/// both the function being altered *and* any callees.
+/// \param m: message to initialise remove_function_pointers with
+/// \param goto_model_function: function to transform
+/// \param function_is_stub: function that will be used to test whether a given
+///   callee has been or will be given a body. It should return true if so, or
+///   false if the function will remain a bodyless stub.
+void remove_returns(
+  goto_model_functiont &goto_model_function,
+  message_handlert &m,
+  function_is_stubt function_is_stub);
+
+void remove_returns(goto_modelt &goto_model, message_handlert &m);
 
 // reverse the above operations
 void restore_returns(symbol_table_baset &, goto_functionst &);
 
-void restore_returns(goto_modelt &);
+void restore_returns(goto_modelt &goto_model, message_handlert &m);
 
 /// produces the identifier that is used to store the return
 /// value of the function with the given identifier
diff --git a/src/util/type.h b/src/util/type.h
index 7f38fc5a335..2104929dcee 100644
--- a/src/util/type.h
+++ b/src/util/type.h
@@ -139,6 +139,16 @@ class typet:public irept
 
     validate_type(type, ns, vm);
   }
+
+  void visit(std::function<void(const typet &)> f) const
+  {
+    f(*this);
+    for(const auto &sub_irep : get_sub())
+    {
+      const typet &subtype = static_cast<const typet &>(sub_irep);
+      subtype.visit(f);
+    }
+  }
 };
 
 /// Type with a single subtype.
diff --git a/unit/Makefile b/unit/Makefile
index 46f8ad567aa..702e59fa14f 100644
--- a/unit/Makefile
+++ b/unit/Makefile
@@ -14,6 +14,9 @@ SRC += analyses/ai/ai.cpp \
        analyses/does_remove_const/does_expr_lose_const.cpp \
        analyses/does_remove_const/does_type_preserve_const_correctness.cpp \
        analyses/does_remove_const/is_type_at_least_as_const_as.cpp \
+       analyses/remove_function_pointers.cpp \
+       analyses/remove_function_pointers_refine.cpp \
+       analyses/remove_returns.cpp \
        big-int/big-int.cpp \
        compound_block_locations.cpp \
        goto-instrument/cover/cover_only.cpp \
diff --git a/unit/analyses/remove_function_pointers.cpp b/unit/analyses/remove_function_pointers.cpp
new file mode 100644
index 00000000000..82377f33e2a
--- /dev/null
+++ b/unit/analyses/remove_function_pointers.cpp
@@ -0,0 +1,129 @@
+/*******************************************************************\
+ Module: Unit tests for module remove_function_pointers
+
+ Author: Diffblue Ltd.
+
+ Date: Apr 2019
+
+\*******************************************************************/
+
+/// \file
+/// Unit tests for module remove_function_pointers
+
+#include <testing-utils/message.h>
+#include <testing-utils/use_catch.h>
+
+#include <util/arith_tools.h>
+#include <util/c_types.h>
+#include <util/std_code.h>
+
+#include <goto-programs/goto_convert_functions.h>
+#include <goto-programs/goto_model.h>
+#include <goto-programs/remove_function_pointers.h>
+
+SCENARIO(
+  "List potential targets works reliable",
+  "[core][goto-programs][list_potential_targets]")
+{
+  goto_modelt goto_model;
+  // create one instance of the function type, they are all
+  // going to have the same signature
+  typet func_type = code_typet{{}, empty_typet{}};
+  // create an empty code block, to act as the functions' body
+  code_blockt func_body = code_blockt{};
+
+  // void f(){};
+  symbolt f;
+  f.name = "f";
+  f.mode = ID_C;
+  f.type = func_type; // void, takes no params
+  f.value = func_body;
+  goto_model.symbol_table.add(f);
+
+  // void g(){};
+  symbolt g;
+  g.name = "g";
+  g.mode = ID_C;
+  g.type = func_type; // void, takes no params
+  g.value = func_body;
+  goto_model.symbol_table.add(g);
+
+  // void h(){};
+  symbolt h;
+  h.name = "h";
+  h.mode = ID_C;
+  h.type = func_type; // void, takes no params
+  h.value = func_body;
+  goto_model.symbol_table.add(h);
+
+  // void l(){};
+  symbolt l;
+  l.name = "l";
+  l.mode = ID_C;
+  l.type = func_type; // void, takes no params
+  l.value = func_body;
+  goto_model.symbol_table.add(l);
+
+  // create array with function pointer elements
+  array_typet fp_array_type(
+    pointer_typet{func_type, 64}, from_integer(4, signed_int_type()));
+  array_exprt fp_array{{}, fp_array_type};
+
+  fp_array.copy_to_operands(address_of_exprt{f.symbol_expr()});
+  fp_array.copy_to_operands(address_of_exprt{g.symbol_expr()});
+  fp_array.copy_to_operands(address_of_exprt{h.symbol_expr()});
+  fp_array.copy_to_operands(address_of_exprt{l.symbol_expr()});
+
+  // f = fparray {f1, f2, f3, f4};
+  symbolt fpa;
+  fpa.name = "f";
+  fpa.mode = ID_C;
+  fpa.type = fp_array_type;
+  fpa.value = fp_array;
+
+  goto_model.symbol_table.add(fpa);
+
+  // pointer to fn call
+  symbolt fn_ptr;
+  fn_ptr.name = "fn_ptr";
+  fn_ptr.mode = ID_C;
+  fn_ptr.type = pointer_typet{func_type, 64};
+  goto_model.symbol_table.add(fn_ptr);
+
+  // symbol for indexing the array
+  symbolt z;
+  z.name = "z";
+  z.mode = ID_C;
+  z.type = signed_int_type();
+  goto_model.symbol_table.add(z);
+
+  // create function with pointer function call instruction
+
+  // void entry(){z; array; fn_ptr = array[z]; *fn_ptr()};
+  symbolt entry;
+  entry.name = "entry";
+  entry.mode = ID_C;
+  entry.type = func_type; // void, takes no params
+
+  code_blockt entry_body{
+    {// fn_ptr = array[z];
+     code_assignt{
+       fn_ptr.symbol_expr(),
+       index_exprt{fp_array, z.symbol_expr(), pointer_type(func_type)}},
+     // *fn_ptr();
+     code_function_callt{dereference_exprt{fn_ptr.symbol_expr()}}}};
+  entry.value = entry_body;
+  goto_model.symbol_table.add(entry);
+
+  WHEN("list_potential_targets is run")
+  {
+    goto_convert(goto_model, null_message_handler);
+    auto target_map =
+      get_function_pointer_targets(null_message_handler, goto_model);
+    THEN("there should be 4 targets recognised")
+    {
+      REQUIRE(target_map.size() == 1);
+      REQUIRE(target_map.begin()->second.size() == 4);
+    }
+  }
+}
diff --git a/unit/analyses/remove_function_pointers_refine.cpp b/unit/analyses/remove_function_pointers_refine.cpp
new file mode 100644
index 00000000000..8913dfd3ab6
--- /dev/null
+++ b/unit/analyses/remove_function_pointers_refine.cpp
@@ -0,0 +1,157 @@
+/*******************************************************************\
+ Module: Unit tests for module remove_function_pointers.refine_call_type
+
+ Author: Diffblue Ltd.
+
+ Date: May 2019
+
+\*******************************************************************/
+
+/// \file
+/// Unit tests for module remove_function_pointers
+
+#include <testing-utils/message.h>
+#include <testing-utils/use_catch.h>
+
+#include <util/arith_tools.h>
+#include <util/c_types.h>
+#include <util/std_code.h>
+
+#include <goto-programs/goto_convert_functions.h>
+#include <goto-programs/goto_model.h>
+#include <goto-programs/remove_function_pointers.h>
+
+SCENARIO(
+  "List potential targets works for ellipsis",
+  "[core][goto-programs][list_potential_targets]")
+{
+  goto_modelt goto_model;
+  // create one instance of the function type, they are all
+  // going to have the same signature
+
+  symbolt int_param;
+  int_param.name = "int_param";
+  int_param.mode = ID_C;
+  int_param.type = signedbv_typet{32};
+  goto_model.symbol_table.add(int_param);
+
+  code_typet::parameterst parameters;
+  parameters.emplace_back(signedbv_typet{32});
+  parameters.back().set_identifier("int_param");
+  auto func_empty_type = code_typet{{}, empty_typet{}};
+  auto func_ellipsis_type = code_typet{{}, empty_typet{}};
+  func_ellipsis_type.make_ellipsis();
+  auto func_one_arg_type = code_typet{parameters, empty_typet{}};
+  // create an empty code block, to act as the functions' body
+  code_blockt func_body = code_blockt{};
+
+  irep_idt f_name{"f"};
+
+  // void f(...){};
+  symbolt f;
+  f.name = f_name;
+  f.mode = ID_C;
+  f.type = func_ellipsis_type; // takes anything
+  f.value = func_body;
+  goto_model.symbol_table.add(f);
+
+  // void g(int){};
+  symbolt g;
+  g.name = "g";
+  g.mode = ID_C;
+  g.type = func_one_arg_type; // takes one int
+  g.value = func_body;
+  goto_model.symbol_table.add(g);
+
+  // create array with function pointer elements
+  array_typet fp_array_type(
+    pointer_typet{func_ellipsis_type, 64}, from_integer(2, index_type()));
+  array_exprt fp_array{{}, fp_array_type};
+
+  fp_array.copy_to_operands(address_of_exprt{f.symbol_expr()});
+  fp_array.copy_to_operands(address_of_exprt{g.symbol_expr()});
+
+  // fpa = fparray {f1, f2};
+  symbolt fpa;
+  fpa.name = "fpa";
+  fpa.mode = ID_C;
+  fpa.type = fp_array_type;
+  fpa.value = fp_array;
+
+  goto_model.symbol_table.add(fpa);
+
+  irep_idt fn_ptr_name{"fn_ptr"};
+
+  // pointer to fn call
+  symbolt fn_ptr;
+  fn_ptr.name = fn_ptr_name;
+  fn_ptr.mode = ID_C;
+  fn_ptr.type = pointer_typet{func_ellipsis_type, 64};
+  goto_model.symbol_table.add(fn_ptr);
+
+  // symbol for indexing the array
+  symbolt z;
+  z.name = "z";
+  z.mode = ID_C;
+  z.type = index_type();
+  goto_model.symbol_table.add(z);
+
+  // create function with pointer function call instruction
+
+  // void entry(){z; array; fn_ptr = array[z]; *fn_ptr(z)};
+  symbolt entry;
+  entry.name = "entry";
+  entry.mode = ID_C;
+  entry.type = func_empty_type;
+
+  code_function_callt::argumentst arguments;
+  arguments.emplace_back(z.symbol_expr());
+
+  code_blockt entry_body{
+    {// fn_ptr = array[z];
+     code_assignt{fn_ptr.symbol_expr(),
+                  index_exprt{fp_array,
+                              z.symbol_expr(),
+                              pointer_type(func_ellipsis_type)}},
+     // *fn_ptr();
+     code_function_callt{dereference_exprt{fn_ptr.symbol_expr()}, arguments}}};
+  entry.value = entry_body;
+  goto_model.symbol_table.add(entry);
+
+  WHEN("list_potential_targets is run")
+  {
+    goto_convert(goto_model, null_message_handler);
+
+    // goto convert removes ellipsis so we need to re-insert them
+    auto &f_symbol = goto_model.symbol_table.get_writeable_ref(f_name);
+    to_code_type(f_symbol.type).make_ellipsis();
+    auto &fn_ptr_symbol =
+      goto_model.symbol_table.get_writeable_ref(fn_ptr_name);
+    to_code_type(fn_ptr_symbol.type.subtype()).make_ellipsis();
+
+    auto &goto_functions = goto_model.goto_functions;
+    for(auto &goto_function_pair : goto_functions.function_map)
+    {
+      auto &goto_function = goto_function_pair.second;
+      auto &goto_program = goto_function.body;
+      for(auto &instruction : goto_program.instructions)
+      {
+        if(instruction.is_function_call())
+        {
+          code_function_callt function_call = instruction.get_function_call();
+          auto &function = to_dereference_expr(function_call.function());
+          to_code_type(function.type()).make_ellipsis();
+          instruction.set_function_call(function_call);
+        }
+      }
+    }
+
+    auto target_map =
+      get_function_pointer_targets(null_message_handler, goto_model);
+    THEN("there should be 4 targets recognised")
+    {
+      REQUIRE(target_map.size() == 1);
+      REQUIRE(target_map.begin()->second.size() == 2);
+    }
+  }
+}
diff --git a/unit/analyses/remove_returns.cpp b/unit/analyses/remove_returns.cpp
new file mode 100644
index 00000000000..8c4c221c414
--- /dev/null
+++ b/unit/analyses/remove_returns.cpp
@@ -0,0 +1,93 @@
+/*******************************************************************\
+ Module: Unit tests for module remove_returns
+
+ Author: Diffblue Ltd.
+
+ Date: Apr 2019
+
+\*******************************************************************/
+
+/// \file
+/// Unit tests for module remove_returns
+/// This is testing the top level interfaces for now.
+
+#include <testing-utils/message.h>
+#include <testing-utils/use_catch.h>
+
+#include <util/arith_tools.h>
+#include <util/c_types.h>
+#include <util/std_code.h>
+
+#include <goto-programs/goto_convert_functions.h>
+#include <goto-programs/goto_model.h>
+#include <goto-programs/remove_returns.h>
+
+// scenario for testing remove returns
+
+SCENARIO(
+  "Remove returns is working reliably",
+  "[core][goto-programs][remove_returns]")
+{
+  goto_modelt goto_model;
+
+  // int f() { return 5; }
+  symbolt f;
+  f.name = "f";
+  f.mode = ID_C;
+  f.type = code_typet{{}, signed_int_type()};
+  f.value = code_blockt{{code_returnt(from_integer(5, signed_int_type()))}};
+  goto_model.symbol_table.add(f);
+
+  goto_convert(goto_model, null_message_handler);
+
+  WHEN("remove_returns is invoked")
+  {
+    remove_returns(
+      goto_model.symbol_table, null_message_handler, goto_model.goto_functions);
+    THEN("function f should not contain any return instructions")
+    {
+      const auto &goto_functions = goto_model.goto_functions;
+      for(const auto &function_pair : goto_functions.function_map)
+      {
+        if(function_pair.first == "f")
+        {
+          const auto &instructions = function_pair.second.body.instructions;
+          for(auto target = instructions.begin(); target != instructions.end();
+              target++)
+          {
+            // make sure there are no return instructions.
+            REQUIRE(!target->is_return());
+          }
+        }
+      }
+    }
+  }
+
+  WHEN("restore_returns is invoked")
+  {
+    restore_returns(goto_model, null_message_handler);
+    THEN("function f should have a skip instruction")
+    {
+      int number_of_returns = 0;
+      const auto &goto_functions = goto_model.goto_functions;
+      for(const auto &function_pair : goto_functions.function_map)
+      {
+        if(function_pair.first == "f")
+        {
+          const auto &instructions = function_pair.second.body.instructions;
+          for(auto target = instructions.begin(); target != instructions.end();
+              target++)
+          {
+            if(target->is_return())
+              number_of_returns++;
+          }
+        }
+      }
+
+      // ensure that there were only 1 return instructions in f
+      REQUIRE(number_of_returns == 1);
+    }
+  }
+}
+
+// scenario for testing restore returns