Extract draw_edges_from_ret_to_jsr function

Author: romainbrenguier

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -1091,17 +1091,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
       ret_instructions.push_back(i_it);
     }
   }
-
-  // Draw edges from every `ret` to every `jsr` successor. Could do better with
-  // flow analysis to distinguish multiple subroutines within the same function.
-  for(const auto retinst : ret_instructions)
-  {
-    auto &a_entry=address_map.at(retinst->address);
-    a_entry.successors.insert(
-      a_entry.successors.end(),
-      jsr_ret_targets.begin(),
-      jsr_ret_targets.end());
-  }
+  draw_edges_from_ret_to_jsr(address_map, jsr_ret_targets, ret_instructions);
 
   for(const auto &address : address_map)
   {
@@ -2719,6 +2709,22 @@ codet java_bytecode_convert_methodt::convert_instructions(
   return code;
 }
 
+void java_bytecode_convert_methodt::draw_edges_from_ret_to_jsr(
+  java_bytecode_convert_methodt::address_mapt &address_map,
+  const std::vector<unsigned int> &jsr_ret_targets,
+  const std::vector<
+    std::vector<java_bytecode_parse_treet::instructiont>::const_iterator>
+    &ret_instructions) const
+{ // Draw edges from every `ret` to every `jsr` successor. Could do better with
+  // flow analysis to distinguish multiple subroutines within the same function.
+  for(const auto &retinst : ret_instructions)
+  {
+    auto &a_entry = address_map.at(retinst->address);
+    a_entry.successors.insert(
+      a_entry.successors.end(), jsr_ret_targets.begin(), jsr_ret_targets.end());
+  }
+}
+
 std::vector<unsigned> java_bytecode_convert_methodt::try_catch_handler(
   const unsigned int address,
   const java_bytecode_parse_treet::methodt::exception_tablet &exception_table)

jbmc/src/java_bytecode/java_bytecode_convert_method_class.h

@@ -279,4 +279,12 @@ class java_bytecode_convert_methodt:public messaget
     const java_bytecode_parse_treet::methodt::exception_tablet &exception_table)
     const;
 
+  void draw_edges_from_ret_to_jsr(
+    address_mapt &address_map,
+    const std::vector<unsigned int> &jsr_ret_targets,
+    const std::vector<
+      std::vector<java_bytecode_parse_treet::instructiont>::const_iterator>
+      &ret_instructions) const;
+};
+
 #endif