Extract convert_dup2_x1 function

Author: romainbrenguier

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

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

jbmc/src/java_bytecode/java_bytecode_convert_method_class.h

@@ -459,6 +459,9 @@ class java_bytecode_convert_methodt:public messaget
     const exprt &arg0,
     exprt::operandst &results) const;
 
+  void
+  convert_dup2_x1(exprt::operandst &op, exprt::operandst &results);
+
   void convert_dup2(exprt::operandst &op, exprt::operandst &results);
 };
 #endif