Correct types of format argument allocation

regression/strings-smoke-tests/java_format/test.desc

@@ -6,3 +6,4 @@ test.class
 ^\[.*assertion.1\].* line 6.* SUCCESS$
 ^\[.*assertion.2\].* line 7.* FAILURE$
 --
+^ignoring

regression/strings-smoke-tests/java_format2/test.desc

@@ -6,3 +6,4 @@ test.class
 ^\[.*assertion.1\].* line 6.* SUCCESS$
 ^\[.*assertion.2\].* line 7.* FAILURE$
 --
+^warning

regression/strings-smoke-tests/java_format3/test.desc

@@ -6,3 +6,4 @@ test.class
 ^\[.*assertion.1\].* line 7.* SUCCESS$
 ^\[.*assertion.2\].* line 9.* FAILURE$
 --
+^warning

src/java_bytecode/java_object_factory.cpp

@@ -178,7 +178,7 @@ class java_object_factoryt
 /// allocate_object() and also in the library preprocessing for allocating
 /// strings.
 /// \param target_expr: expression to which the necessary memory will be
-///   allocated
+///   allocated, its type should be pointer to `allocate_type`
 /// \param allocate_type: type of the object allocated
 /// \param symbol_table: symbol table
 /// \param loc: location in the source
@@ -243,32 +243,27 @@ exprt allocate_dynamic_object(
 /// and which takes care of creating the associated declarations.
 /// \param target_expr: expression to which the necessary memory will be
 ///   allocated
-/// \param allocate_type: type of the object allocated
 /// \param symbol_table: symbol table
 /// \param loc: location in the source
 /// \param output_code: code block to which the necessary code is added
-/// \param cast_needed: Boolean flags saying where we need to cast the malloc
-///   site
-/// \return Expression representing the malloc site allocated.
-exprt allocate_dynamic_object_with_decl(
+void allocate_dynamic_object_with_decl(
   const exprt &target_expr,
-  const typet &allocate_type,
   symbol_tablet &symbol_table,
   const source_locationt &loc,
-  code_blockt &output_code,
-  bool cast_needed)
+  code_blockt &output_code)
 {
   std::vector<const symbolt *> symbols_created;
-
   code_blockt tmp_block;
-  exprt result=allocate_dynamic_object(
+  const typet &allocate_type=target_expr.type().subtype();
+  // We will not use the malloc site and can safely ignore it
+  (void) allocate_dynamic_object(
     target_expr,
     allocate_type,
     symbol_table,
     loc,
     tmp_block,
     symbols_created,
-    cast_needed);
+    false);
 
   // Add the following code to output_code for each symbol that's been created:
   //   <type> <identifier>;
@@ -281,8 +276,6 @@ exprt allocate_dynamic_object_with_decl(
 
   for(const exprt &code : tmp_block.operands())
     output_code.add(to_code(code));
-
-  return result;
 }
 
 /// Installs a new symbol in the symbol table, pushing the corresponding symbolt

src/java_bytecode/java_object_factory.h

@@ -149,12 +149,10 @@ exprt allocate_dynamic_object(
   std::vector<const symbolt *> &symbols_created,
   bool cast_needed=false);
 
-exprt allocate_dynamic_object_with_decl(
+void allocate_dynamic_object_with_decl(
   const exprt &target_expr,
-  const typet &allocate_type,
   symbol_tablet &symbol_table,
   const source_locationt &loc,
-  code_blockt &output_code,
-  bool cast_needed=false);
+  code_blockt &output_code);
 
 #endif // CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_H

src/java_bytecode/java_string_library_preprocess.cpp

@@ -575,8 +575,7 @@ exprt java_string_library_preprocesst::allocate_fresh_string(
 {
   exprt str=fresh_string(type, loc, symbol_table);
   code.add(code_declt(str));
-  (void) allocate_dynamic_object_with_decl(
-    str, str.type().subtype(), symbol_table, loc, code, false);
+  allocate_dynamic_object_with_decl(str, symbol_table, loc, code);
   return str;
 }
 
@@ -594,8 +593,7 @@ exprt java_string_library_preprocesst::allocate_fresh_array(
 {
   exprt array=fresh_array(type, loc, symbol_table);
   code.add(code_declt(array));
-  (void) allocate_dynamic_object_with_decl(
-    array, array.type().subtype(), symbol_table, loc, code, false);
+  allocate_dynamic_object_with_decl(array, symbol_table, loc, code);
   return array;
 }
 
@@ -1389,10 +1387,9 @@ exprt java_string_library_preprocesst::make_argument_for_format(
   // arg_i = argv[index]
   exprt obj=get_object_at_index(argv, index);
   symbolt object_symbol=get_fresh_aux_symbol(
-    obj.type(), "tmp_object", "tmp_object", loc, ID_java, symbol_table);
+    obj.type(), "tmp_format_obj", "tmp_format_obj", loc, ID_java, symbol_table);
   symbol_exprt arg_i=object_symbol.symbol_expr();
-  (void) allocate_dynamic_object_with_decl(
-    arg_i, obj.type(), symbol_table, loc, code, false);
+  allocate_dynamic_object_with_decl(arg_i, symbol_table, loc, code);
   code.add(code_assignt(arg_i, obj));
   code.add(code_assumet(not_exprt(equal_exprt(
     arg_i, null_pointer_exprt(to_pointer_type(arg_i.type()))))));