Skip to content

Commit c1e0d0c

Browse files
committed
Use allocate_objectst in java string library preprocessing
1 parent d84530e commit c1e0d0c

File tree

1 file changed

+23
-3
lines changed

1 file changed

+23
-3
lines changed

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

Lines changed: 23 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@ 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>
2021
#include <util/std_expr.h>
2122
#include <util/std_code.h>
@@ -574,7 +575,17 @@ 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(
580+
ID_java,
581+
loc,
582+
function_id,
583+
symbol_table);
584+
585+
allocate_objects.allocate_dynamic_object_with_decl(
586+
str,
587+
code);
588+
578589
return str;
579590
}
580591

@@ -1366,8 +1377,17 @@ exprt java_string_library_preprocesst::make_argument_for_format(
13661377
ID_java,
13671378
symbol_table);
13681379
symbol_exprt arg_i=object_symbol.symbol_expr();
1369-
allocate_dynamic_object_with_decl(
1370-
arg_i, symbol_table, loc, function_id, code);
1380+
1381+
allocate_objectst allocate_objects(
1382+
ID_java,
1383+
loc,
1384+
function_id,
1385+
symbol_table);
1386+
1387+
allocate_objects.allocate_dynamic_object_with_decl(
1388+
arg_i,
1389+
code);
1390+
13711391
code.add(code_assignt(arg_i, obj), loc);
13721392
code.add(
13731393
code_assumet(

0 commit comments

Comments
 (0)