JBMC: remove return values on a per-function basis

Author: smowton

src/jbmc/jbmc_parse_options.cpp

@@ -642,7 +642,8 @@ int jbmc_parse_optionst::get_goto_program(
 }
 
 void jbmc_parse_optionst::process_goto_function(
-  goto_model_functiont &function)
+  goto_model_functiont &function,
+  const can_produce_functiont &available_functions)
 {
   symbol_tablet &symbol_table = function.get_symbol_table();
   goto_functionst::goto_functiont &goto_function = function.get_goto_function();
@@ -655,6 +656,14 @@ void jbmc_parse_optionst::process_goto_function(
     remove_instanceof(goto_function, symbol_table);
     // Java virtual functions -> explicit dispatch tables:
     remove_virtual_functions(function);
+
+    auto function_is_stub =
+      [&symbol_table, &available_functions](const irep_idt &id) { // NOLINT(*)
+        return symbol_table.lookup_ref(id).value.is_nil() &&
+               !available_functions.can_produce_function(id);
+      };
+
+    remove_returns(function, function_is_stub);
   }
 
   catch(const char *e)
@@ -692,9 +701,6 @@ bool jbmc_parse_optionst::process_goto_functions(
     // instrument library preconditions
     instrument_preconditions(goto_model);
 
-    // remove returns, gcc vectors, complex
-    remove_returns(goto_model);
-
     // Similar removal of java nondet statements:
     // TODO Should really get this from java_bytecode_language somehow, but we
     // don't have an instance of that here.

src/jbmc/jbmc_parse_options.h

@@ -19,6 +19,7 @@ Author: Daniel Kroening, [email protected]
 #include <analyses/goto_check.h>
 
 #include <goto-programs/goto_trace.h>
+#include <goto-programs/lazy_goto_model.h>
 
 #include <java_bytecode/java_bytecode_language.h>
 
@@ -83,7 +84,9 @@ class jbmc_parse_optionst:
     const char **argv,
     const std::string &extra_options);
 
-  void process_goto_function(goto_model_functiont &function);
+  void process_goto_function(
+    goto_model_functiont &function,
+    const can_produce_functiont &);
   bool process_goto_functions(goto_modelt &goto_model, const optionst &options);
 
 protected: