Skip to content

Commit f071684

Browse files
committed
Use allocate_objectst in jbmc
1 parent 2fdf70e commit f071684

8 files changed

+135
-361
lines changed

jbmc/src/java_bytecode/convert_java_nondet.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -55,7 +55,7 @@ static goto_programt get_gen_nondet_init_instructions(
5555
symbol_table,
5656
source_loc,
5757
skip_classid,
58-
allocation_typet::DYNAMIC,
58+
lifetimet::DYNAMIC,
5959
object_factory_parameters,
6060
update_in_placet::NO_UPDATE_IN_PLACE);
6161

jbmc/src/java_bytecode/java_entry_point.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -243,7 +243,7 @@ static void java_static_lifetime_init(
243243
symbol_table,
244244
source_location,
245245
false,
246-
allocation_typet::GLOBAL,
246+
lifetimet::STATIC_GLOBAL,
247247
parameters,
248248
pointer_type_selector,
249249
update_in_placet::NO_UPDATE_IN_PLACE);
@@ -348,7 +348,7 @@ exprt::operandst java_build_arguments(
348348
init_code,
349349
symbol_table,
350350
parameters,
351-
allocation_typet::LOCAL,
351+
lifetimet::AUTOMATIC_LOCAL,
352352
function.location,
353353
pointer_type_selector);
354354
}
@@ -394,7 +394,7 @@ exprt::operandst java_build_arguments(
394394
init_code_for_type,
395395
symbol_table,
396396
parameters,
397-
allocation_typet::DYNAMIC,
397+
lifetimet::DYNAMIC,
398398
function.location,
399399
pointer_type_selector);
400400
init_code_for_type.add(

0 commit comments

Comments
 (0)