JBMC: remove return values on a per-function basis

Author: smowton

src/jbmc/jbmc_parse_options.cpp

@@ -649,6 +649,8 @@ void jbmc_parse_optionst::process_goto_function(
     remove_instanceof(goto_function, symbol_table);
     // Java virtual functions -> explicit dispatch tables:
     remove_virtual_functions(function);
+    // remove returns
+    remove_returns(function);
   }
 
   catch(const char *e)
@@ -686,9 +688,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.