Extract convert_monitorenter function

Author: romainbrenguier

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -1929,17 +1929,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
     }
     else if(statement=="monitorenter")
     {
-      // becomes a function call
-      code_typet type;
-      type.return_type()=void_typet();
-      type.parameters().resize(1);
-      type.parameters()[0].type()=java_reference_type(void_typet());
-      code_function_callt call;
-      call.function()=symbol_exprt("java::monitorenter", type);
-      call.lhs().make_nil();
-      call.arguments().push_back(op[0]);
-      call.add_source_location()=i_it->source_location;
-      c=call;
+      c = convert_monitorenter(i_it->source_location, op);
     }
     else if(statement=="monitorexit")
     {
@@ -2310,6 +2300,22 @@ codet java_bytecode_convert_methodt::convert_instructions(
   return code;
 }
 
+codet java_bytecode_convert_methodt::convert_monitorenter(
+  const source_locationt &location,
+  const exprt::operandst &op) const
+{
+  code_typet type;
+  type.return_type() = void_typet();
+  type.parameters().resize(1);
+  type.parameters()[0].type() = java_reference_type(void_typet());
+  code_function_callt call;
+  call.function() = symbol_exprt("java::monitorenter", type);
+  call.lhs().make_nil();
+  call.arguments().push_back(op[0]);
+  call.add_source_location() = location;
+  return call;
+}
+
 void java_bytecode_convert_methodt::convert_multianewarray(
   const source_locationt &location,
   const exprt &arg0,

jbmc/src/java_bytecode/java_bytecode_convert_method_class.h

@@ -416,5 +416,9 @@ class java_bytecode_convert_methodt:public messaget
     const exprt::operandst &op,
     codet &c,
     exprt::operandst &results);
+
+  codet convert_monitorenter(
+    const source_locationt &location,
+    const exprt::operandst &op) const;
 };
 #endif