Merge pull request #3443 from danpoe/refactor/factor-out-object-allocation-from-object-factories

Factor out object allocation from object factories [blocks: #3455]

Author: danpoe

jbmc/src/java_bytecode/convert_java_nondet.cpp

@@ -55,7 +55,7 @@ static goto_programt get_gen_nondet_init_instructions(
     symbol_table,
     source_loc,
     skip_classid,
-    allocation_typet::DYNAMIC,
+    lifetimet::DYNAMIC,
     object_factory_parameters,
     update_in_placet::NO_UPDATE_IN_PLACE);
 

jbmc/src/java_bytecode/java_entry_point.cpp

@@ -243,7 +243,7 @@ static void java_static_lifetime_init(
           symbol_table,
           source_location,
           false,
-          allocation_typet::GLOBAL,
+          lifetimet::STATIC_GLOBAL,
           parameters,
           pointer_type_selector,
           update_in_placet::NO_UPDATE_IN_PLACE);
@@ -348,7 +348,7 @@ exprt::operandst java_build_arguments(
         init_code,
         symbol_table,
         parameters,
-        allocation_typet::LOCAL,
+        lifetimet::AUTOMATIC_LOCAL,
         function.location,
         pointer_type_selector);
     }
@@ -394,7 +394,7 @@ exprt::operandst java_build_arguments(
           init_code_for_type,
           symbol_table,
           parameters,
-          allocation_typet::DYNAMIC,
+          lifetimet::DYNAMIC,
           function.location,
           pointer_type_selector);
         init_code_for_type.add(