From 58ef65b7aa78d3ef28acd42c19e77c21a7f4f1d7 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Mon, 2 Oct 2017 15:20:16 +0100 Subject: [PATCH] Object factory: initialise global symbols in place This eliminates a misleading attribution of global symbols to __CPROVER_start, which could lead to their elimination by replace_entry_pointt. --- src/java_bytecode/java_entry_point.cpp | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) diff --git a/src/java_bytecode/java_entry_point.cpp b/src/java_bytecode/java_entry_point.cpp index e456556c258..17c7b5f96ed 100644 --- a/src/java_bytecode/java_entry_point.cpp +++ b/src/java_bytecode/java_entry_point.cpp @@ -125,18 +125,17 @@ void java_static_lifetime_init( if(allow_null && is_non_null_library_global(nameid)) allow_null=false; } - auto newsym=object_factory( - sym.type, - symname, + gen_nondet_init( + sym.symbol_expr(), code_block, - allow_null, symbol_table, - object_factory_parameters, - allocation_typet::GLOBAL, source_location, - pointer_type_selector); - code_assignt assignment(sym.symbol_expr(), newsym); - code_block.add(assignment); + false, + allocation_typet::GLOBAL, + allow_null, + object_factory_parameters, + pointer_type_selector, + update_in_placet::NO_UPDATE_IN_PLACE); } else if(sym.value.is_not_nil()) {