@@ -16,13 +16,14 @@ Date: April 2017
16
16
// / java standard library. In particular methods from java.lang.String,
17
17
// / java.lang.StringBuilder, java.lang.StringBuffer.
18
18
19
+ #include < util/allocate_objects.h>
19
20
#include < util/arith_tools.h>
20
- #include < util/std_expr.h>
21
- #include < util/std_code.h>
21
+ #include < util/c_types.h>
22
22
#include < util/fresh_symbol.h>
23
23
#include < util/refined_string_type.h>
24
+ #include < util/std_code.h>
25
+ #include < util/std_expr.h>
24
26
#include < util/string_expr.h>
25
- #include < util/c_types.h>
26
27
27
28
#include " java_types.h"
28
29
#include " java_object_factory.h"
@@ -574,7 +575,11 @@ exprt java_string_library_preprocesst::allocate_fresh_string(
574
575
code_blockt &code)
575
576
{
576
577
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
+
578
583
return str;
579
584
}
580
585
@@ -1366,8 +1371,11 @@ exprt java_string_library_preprocesst::make_argument_for_format(
1366
1371
ID_java,
1367
1372
symbol_table);
1368
1373
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
+
1371
1379
code.add (code_assignt (arg_i, obj), loc);
1372
1380
code.add (
1373
1381
code_assumet (
0 commit comments