Extract convert_dup2 function

Author: romainbrenguier

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -1487,14 +1487,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
     else if(statement=="dup2")
     {
       PRECONDITION(!stack.empty() && results.empty());
-
-      if(get_bytecode_type_width(stack.back().type())==32)
-        op=pop(2);
-      else
-        op=pop(1);
-
-      results.insert(results.end(), op.begin(), op.end());
-      results.insert(results.end(), op.begin(), op.end());
+      convert_dup2(op, results);
     }
     else if(statement=="dup2_x1")
     {
@@ -1956,6 +1949,19 @@ codet java_bytecode_convert_methodt::convert_instructions(
   return code;
 }
 
+void java_bytecode_convert_methodt::convert_dup2(
+  exprt::operandst &op,
+  exprt::operandst &results)
+{
+  if(get_bytecode_type_width(stack.back().type()) == 32)
+    op = pop(2);
+  else
+    op = pop(1);
+
+  results.insert(results.end(), op.begin(), op.end());
+  results.insert(results.end(), op.begin(), op.end());
+}
+
 exprt::operandst &java_bytecode_convert_methodt::convert_const(
   const irep_idt &statement,
   exprt &arg0,

jbmc/src/java_bytecode/java_bytecode_convert_method_class.h

@@ -456,5 +456,7 @@ class java_bytecode_convert_methodt:public messaget
     const irep_idt &statement,
     exprt &arg0,
     exprt::operandst &results) const;
+
+  void convert_dup2(exprt::operandst &op, exprt::operandst &results);
 };
 #endif