Extract try_catch_handler function

romainbrenguier · romainbrenguier · commit 390063f06b2c · 2018-06-13T09:07:31.000+01:00
diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -1034,18 +1034,11 @@ codet java_bytecode_convert_methodt::convert_instructions(
        i_it->statement=="invokespecial" ||
        i_it->statement=="invokeinterface")
     {
-      // find the corresponding try-catch blocks and add the handlers
-      // to the targets
-      for(const auto &exception_row : method.exception_table)
-      {
-        if(i_it->address>=exception_row.start_pc &&
-           i_it->address<exception_row.end_pc)
-        {
-          a_entry.first->second.successors.push_back(
-            exception_row.handler_pc);
-          targets.insert(exception_row.handler_pc);
-        }
-      }
+      const std::vector<unsigned int> handler =
+        try_catch_handler(i_it->address, method.exception_table);
+      std::list<unsigned int> &successors = a_entry.first->second.successors;
+      successors.insert(successors.end(), handler.begin(), handler.end());
+      targets.insert(handler.begin(), handler.end());
     }
 
     if(i_it->statement=="goto" ||
@@ -2726,6 +2719,20 @@ codet java_bytecode_convert_methodt::convert_instructions(
   return code;
 }
 
+std::vector<unsigned> java_bytecode_convert_methodt::try_catch_handler(
+  const unsigned int address,
+  const java_bytecode_parse_treet::methodt::exception_tablet &exception_table)
+  const
+{
+  std::vector<unsigned> result;
+  for(const auto &exception_row : exception_table)
+  {
+    if(address >= exception_row.start_pc && address < exception_row.end_pc)
+      result.push_back(exception_row.handler_pc);
+  }
+  return result;
+}
+
 /// This uses a cut-down version of the logic in
 /// java_bytecode_convert_methodt::convert to initialize symbols for the
 /// parameters and update the parameters in the type of method_symbol with
diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h b/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h
@@ -273,6 +273,10 @@ class java_bytecode_convert_methodt:public messaget
     const typet &,
     code_blockt &,
     exprt &);
-};
+
+  std::vector<unsigned int> try_catch_handler(
+    unsigned int address,
+    const java_bytecode_parse_treet::methodt::exception_tablet &exception_table)
+    const;
 
 #endif
