Skip to content

Commit a2d7811

Browse files
Use dynamic object instead of tmp_object in init
In initialisation of string objects, this prevents the created objects from getting out of scope.
1 parent daef30f commit a2d7811

File tree

1 file changed

+6
-9
lines changed

1 file changed

+6
-9
lines changed

src/java_bytecode/java_object_factory.cpp

+6-9
Original file line numberDiff line numberDiff line change
@@ -637,17 +637,14 @@ static bool add_nondet_string_pointer_initialization(
637637
if(!struct_type.has_component("data") || !struct_type.has_component("length"))
638638
return true;
639639

640-
const symbolt tmp_object_sym = new_tmp_symbol(symbol_table, loc, struct_type);
641-
// Note that it is fine to use a tmp_object here as this should only be used
642-
// in __CPROVER_start whose scope covers all the program execution.
643-
const symbol_exprt tmp_object = tmp_object_sym.symbol_expr();
644-
// struct java.lang.String tmp_object;
645-
code.add(code_declt(tmp_object));
640+
allocate_dynamic_object_with_decl(expr, symbol_table, loc, code);
641+
646642
code.add(
647643
initialize_nondet_string_struct(
648-
tmp_object, max_nondet_string_length, loc, symbol_table));
649-
// expr = &tmp_object;
650-
code.add(code_assignt(expr, address_of_exprt(tmp_object), loc));
644+
dereference_exprt(expr, struct_type),
645+
max_nondet_string_length,
646+
loc,
647+
symbol_table));
651648
return false;
652649
}
653650

0 commit comments

Comments
 (0)