Skip to content

Commit 65835c2

Browse files
committed
Object factory: support global allocation
This already supported choosing between allocation on the stack and the heap; this adds global object creation as a new possibility. java_static_lifetime_init is switched to use global allocation, as this reflects the true lifetime of static fields.
1 parent 9d08aa6 commit 65835c2

File tree

5 files changed

+107
-79
lines changed

5 files changed

+107
-79
lines changed

src/goto-programs/convert_nondet.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -85,7 +85,7 @@ static goto_programt::targett insert_nondet_init_code(
8585
symbol_table,
8686
source_loc,
8787
true,
88-
true,
88+
allocation_typet::DYNAMIC,
8989
!nullable,
9090
max_nondet_array_length,
9191
update_in_placet::NO_UPDATE_IN_PLACE);

src/java_bytecode/java_bytecode_instrument.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -113,6 +113,7 @@ codet java_bytecode_instrumentt::throw_exception(
113113
false,
114114
symbol_table,
115115
max_array_length,
116+
allocation_typet::LOCAL,
116117
original_loc);
117118
}
118119
else

src/java_bytecode/java_entry_point.cpp

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -118,6 +118,7 @@ void java_static_lifetime_init(
118118
allow_null,
119119
symbol_table,
120120
max_nondet_array_length,
121+
allocation_typet::GLOBAL,
121122
source_location);
122123
code_assignt assignment(sym.symbol_expr(), newsym);
123124
code_block.add(assignment);
@@ -180,6 +181,7 @@ exprt::operandst java_build_arguments(
180181
allow_null,
181182
symbol_table,
182183
max_nondet_array_length,
184+
allocation_typet::LOCAL,
183185
function.location);
184186

185187
// record as an input

0 commit comments

Comments
 (0)