Extract convert_dup2_x1 function

Author: romainbrenguier

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -1492,14 +1492,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")
     {
@@ -1962,6 +1955,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,
   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_x1(exprt::operandst &op, exprt::operandst &results);
+
   void convert_dup2(exprt::operandst &op, exprt::operandst &results);
 };
 #endif