Extract convert_dup2_x2 function

Author: romainbrenguier

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -1497,22 +1497,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
     else if(statement=="dup2_x2")
     {
       PRECONDITION(!stack.empty() && results.empty());
-
-      if(get_bytecode_type_width(stack.back().type())==32)
-        op=pop(2);
-      else
-        op=pop(1);
-
-      exprt::operandst op2;
-
-      if(get_bytecode_type_width(stack.back().type())==32)
-        op2=pop(2);
-      else
-        op2=pop(1);
-
-      results.insert(results.end(), op.begin(), op.end());
-      results.insert(results.end(), op2.begin(), op2.end());
-      results.insert(results.end(), op.begin(), op.end());
+      convert_dup2_x2(op, results);
     }
     else if(statement=="dconst")
     {
@@ -1968,6 +1953,27 @@ void java_bytecode_convert_methodt::convert_dup2_x1(
   results.insert(results.end(), op.begin(), op.end());
 }
 
+void java_bytecode_convert_methodt::convert_dup2_x2(
+  exprt::operandst &op,
+  exprt::operandst &results)
+{
+  if(get_bytecode_type_width(stack.back().type()) == 32)
+    op = pop(2);
+  else
+    op = pop(1);
+
+  exprt::operandst op2;
+
+  if(get_bytecode_type_width(stack.back().type()) == 32)
+    op2 = pop(2);
+  else
+    op2 = pop(1);
+
+  results.insert(results.end(), op.begin(), op.end());
+  results.insert(results.end(), op2.begin(), op2.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

@@ -457,6 +457,8 @@ class java_bytecode_convert_methodt:public messaget
     exprt &arg0,
     exprt::operandst &results) const;
 
+  void convert_dup2_x2(exprt::operandst &op, exprt::operandst &results);
+
   void convert_dup2_x1(exprt::operandst &op, exprt::operandst &results);
 
   void convert_dup2(exprt::operandst &op, exprt::operandst &results);