Extract convert_ifnull function

romainbrenguier · romainbrenguier · commit 61d03da6a6ef · 2018-06-13T09:07:31.000+01:00
diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -1610,16 +1610,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
       mp_integer number;
       bool ret=to_integer(to_constant_expr(arg0), number);
       INVARIANT(!ret, "ifnull argument should be an integer");
-      code_ifthenelset code_branch;
-      const typecast_exprt lhs(op[0], java_reference_type(empty_typet()));
-      const exprt rhs(null_pointer_exprt(to_pointer_type(lhs.type())));
-      code_branch.cond()=binary_relation_exprt(lhs, ID_equal, rhs);
-      code_branch.then_case()=code_gotot(label(integer2string(number)));
-      code_branch.then_case().add_source_location()=
-        address_map.at(integer2unsigned(number)).source->source_location;
-      code_branch.add_source_location()=i_it->source_location;
-
-      c=code_branch;
+      c = convert_ifnull(address_map, op, number, i_it->source_location);
     }
     else if(statement=="iinc")
     {
@@ -2552,6 +2543,23 @@ codet java_bytecode_convert_methodt::convert_instructions(
   return code;
 }
 
+codet java_bytecode_convert_methodt::convert_ifnull(
+  const java_bytecode_convert_methodt::address_mapt &address_map,
+  const exprt::operandst &op,
+  const mp_integer &number,
+  const source_locationt &location) const
+{
+  code_ifthenelset code_branch;
+  const typecast_exprt lhs(op[0], java_reference_type(empty_typet()));
+  const exprt rhs(null_pointer_exprt(to_pointer_type(lhs.type())));
+  code_branch.cond() = binary_relation_exprt(lhs, ID_equal, rhs);
+  code_branch.then_case() = code_gotot(label(integer2string(number)));
+  code_branch.then_case().add_source_location() =
+    address_map.at(integer2unsigned(number)).source->source_location;
+  code_branch.add_source_location() = location;
+  return code_branch;
+}
+
 codet java_bytecode_convert_methodt::convert_ifnonull(
   const java_bytecode_convert_methodt::address_mapt &address_map,
   const exprt::operandst &op,
diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h b/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h
@@ -356,6 +356,12 @@ class java_bytecode_convert_methodt:public messaget
     const mp_integer &number,
     const source_locationt &location) const;
 
+  codet convert_ifnull(
+    const java_bytecode_convert_methodt::address_mapt &address_map,
+    const exprt::operandst &op,
+    const mp_integer &number,
+    const source_locationt &location) const;
+
   codet convert_ifnull(
     java_bytecode_convert_methodt::address_mapt &address_map,
     const exprt::operandst &op,
