@@ -16,13 +16,14 @@ Date: April 2017
1616// / java standard library. In particular methods from java.lang.String,
1717// / java.lang.StringBuilder, java.lang.StringBuffer.
1818
19+ #include < util/allocate_objects.h>
1920#include < util/arith_tools.h>
20- #include < util/std_expr.h>
21- #include < util/std_code.h>
21+ #include < util/c_types.h>
2222#include < util/fresh_symbol.h>
2323#include < util/refined_string_type.h>
24+ #include < util/std_code.h>
25+ #include < util/std_expr.h>
2426#include < util/string_expr.h>
25- #include < util/c_types.h>
2627
2728#include " java_types.h"
2829#include " java_object_factory.h"
@@ -574,7 +575,11 @@ exprt java_string_library_preprocesst::allocate_fresh_string(
574575 code_blockt &code)
575576{
576577 exprt str=fresh_string (type, loc, symbol_table);
577- allocate_dynamic_object_with_decl (str, symbol_table, loc, function_id, code);
578+
579+ allocate_objectst allocate_objects (ID_java, loc, function_id, symbol_table);
580+
581+ allocate_objects.allocate_dynamic_object_with_decl (code, str);
582+
578583 return str;
579584}
580585
@@ -1366,8 +1371,11 @@ exprt java_string_library_preprocesst::make_argument_for_format(
13661371 ID_java,
13671372 symbol_table);
13681373 symbol_exprt arg_i=object_symbol.symbol_expr ();
1369- allocate_dynamic_object_with_decl (
1370- arg_i, symbol_table, loc, function_id, code);
1374+
1375+ allocate_objectst allocate_objects (ID_java, loc, function_id, symbol_table);
1376+
1377+ allocate_objects.allocate_dynamic_object_with_decl (code, arg_i);
1378+
13711379 code.add (code_assignt (arg_i, obj), loc);
13721380 code.add (
13731381 code_assumet (
0 commit comments