Extract convert_pop function

Author: romainbrenguier

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -1601,16 +1601,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
     }
     else if(statement=="pop" || statement=="pop2")
     {
-      // these are skips
-      c=code_skipt();
-
-      // pop2 removes two single-word items from the stack (e.g. two
-      // integers, or an integer and an object reference) or one
-      // two-word item (i.e. a double or a long).
-      // http://cs.au.dk/~mis/dOvs/jvmspec/ref-pop2.html
-      if(statement=="pop2" &&
-         get_bytecode_type_width(op[0].type())==32)
-        pop(1);
+      c = convert_pop(statement, op);
     }
     else if(statement=="instanceof")
     {
@@ -1880,6 +1871,22 @@ codet java_bytecode_convert_methodt::convert_instructions(
   return code;
 }
 
+codet java_bytecode_convert_methodt::convert_pop(
+  const irep_idt &statement,
+  const exprt::operandst &op)
+{
+  // these are skips
+  codet c = code_skipt();
+
+  // pop2 removes two single-word items from the stack (e.g. two
+  // integers, or an integer and an object reference) or one
+  // two-word item (i.e. a double or a long).
+  // http://cs.au.dk/~mis/dOvs/jvmspec/ref-pop2.html
+  if(statement == "pop2" && get_bytecode_type_width(op[0].type()) == 32)
+    pop(1);
+  return c;
+}
+
 codet java_bytecode_convert_methodt::convert_switch(
   java_bytecode_convert_methodt::address_mapt &address_map,
   const std::vector<java_bytecode_parse_treet::instructiont>::const_iterator

jbmc/src/java_bytecode/java_bytecode_convert_method_class.h

@@ -481,5 +481,7 @@ class java_bytecode_convert_methodt:public messaget
     const std::vector<java_bytecode_parse_treet::instructiont>::const_iterator
       &i_it,
     const exprt::operandst &op);
+
+  codet convert_pop(const irep_idt &statement, const exprt::operandst &op);
 };
 #endif