Extract replace_calls_to_cprover_assume function

Author: romainbrenguier

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -1234,24 +1234,14 @@ codet java_bytecode_convert_methodt::convert_instructions(
         results[0] = *res;
       }
     }
-    // replace calls to CProver.assume
     else if(statement=="invokestatic" &&
             id2string(arg0.get(ID_identifier))==
             "java::org.cprover.CProver.assume:(Z)V")
     {
       const code_typet &code_type=to_code_type(arg0.type());
       INVARIANT(code_type.parameters().size()==1,
                 "function expected to have exactly one parameter");
-
-      exprt operand = pop(1)[0];
-      // we may need to adjust the type of the argument
-      if(operand.type()!=bool_typet())
-        operand.make_typecast(bool_typet());
-
-      c=code_assumet(operand);
-      source_locationt loc=i_it->source_location;
-      loc.set_function(method_id);
-      c.add_source_location()=loc;
+      c = replace_call_to_cprover_assume(i_it->source_location, c);
     }
     else if(statement=="invokeinterface" ||
             statement=="invokespecial" ||
@@ -2176,6 +2166,21 @@ codet java_bytecode_convert_methodt::convert_instructions(
   return code;
 }
 
+codet &java_bytecode_convert_methodt::replace_call_to_cprover_assume(
+  source_locationt location,
+  codet &c)
+{
+  exprt operand = pop(1)[0];
+  // we may need to adjust the type of the argument
+  if(operand.type() != bool_typet())
+    operand.make_typecast(bool_typet());
+
+  c = code_assumet(operand);
+  location.set_function(method_id);
+  c.add_source_location() = location;
+  return c;
+}
+
 void java_bytecode_convert_methodt::convert_checkcast(
   const exprt &arg0,
   const exprt::operandst &op,

jbmc/src/java_bytecode/java_bytecode_convert_method_class.h

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