diff --git a/src/goto-cc/linker_script_merge.cpp b/src/goto-cc/linker_script_merge.cpp index 97f37165f9a..aef11c3a5bc 100644 --- a/src/goto-cc/linker_script_merge.cpp +++ b/src/goto-cc/linker_script_merge.cpp @@ -84,20 +84,11 @@ int linker_script_merget::add_linker_script_definitions() << messaget::eom; return fail; } - if( - original_goto_model->goto_functions.function_map.erase( - INITIALIZE_FUNCTION) != 0) + + if(original_goto_model->can_produce_function(INITIALIZE_FUNCTION)) { - static_lifetime_init( - original_goto_model->symbol_table, - original_goto_model->symbol_table.lookup_ref(INITIALIZE_FUNCTION) - .location); - goto_convert( - INITIALIZE_FUNCTION, - original_goto_model->symbol_table, - original_goto_model->goto_functions, - log.get_message_handler()); - original_goto_model->goto_functions.update(); + recreate_initialize_function( + *original_goto_model, log.get_message_handler()); } fail=goto_and_object_mismatch(linker_defined_symbols, linker_values); diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp index e8407519334..af0308edc4a 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp @@ -560,8 +560,8 @@ void dfcct::reinitialize_model() swap_and_wrap.get_swapped_functions(instrumented_functions); log.status() << "Updating init function" << messaget::eom; - utils.create_initialize_function(); - goto_model.goto_functions.update(); + if(goto_model.can_produce_function(INITIALIZE_FUNCTION)) + recreate_initialize_function(goto_model, message_handler); nondet_static(goto_model, to_exclude_from_nondet_static); // Initialize the map of instrumented functions by adding extra instructions diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.cpp index a2a863af064..f0a21c3b254 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.cpp @@ -140,22 +140,6 @@ const symbolt &dfcc_utilst::create_static_symbol( return symbol; } -void dfcc_utilst::create_initialize_function() -{ - if(goto_model.goto_functions.function_map.erase(INITIALIZE_FUNCTION) != 0) - { - static_lifetime_init( - goto_model.symbol_table, - goto_model.symbol_table.lookup_ref(INITIALIZE_FUNCTION).location); - goto_convert( - INITIALIZE_FUNCTION, - goto_model.symbol_table, - goto_model.goto_functions, - message_handler); - goto_model.goto_functions.update(); - } -} - void dfcc_utilst::fix_parameters_symbols(const irep_idt &function_id) { auto &function_symbol = get_function_symbol(function_id); diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.h index 5d9f5319d9e..36aee99ee26 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.h @@ -82,10 +82,6 @@ class dfcc_utilst const exprt &initial_value, const bool no_nondet_initialization = true); - /// Regenerates the CPROVER_INITIALIZE function which defines all global - /// statics of the goto model. - void create_initialize_function(); - /// Creates a new parameter symbol for the given function_id const symbolt &create_new_parameter_symbol( const irep_idt &function_id, diff --git a/src/goto-instrument/contracts/memory_predicates.cpp b/src/goto-instrument/contracts/memory_predicates.cpp index ad0a154c6ba..47108333ab5 100644 --- a/src/goto-instrument/contracts/memory_predicates.cpp +++ b/src/goto-instrument/contracts/memory_predicates.cpp @@ -210,18 +210,8 @@ void is_fresh_baset::add_declarations(const std::string &decl_string) } } - if(goto_model.goto_functions.function_map.erase(INITIALIZE_FUNCTION) != 0) - { - static_lifetime_init( - goto_model.symbol_table, - goto_model.symbol_table.lookup_ref(INITIALIZE_FUNCTION).location); - goto_convert( - INITIALIZE_FUNCTION, - goto_model.symbol_table, - goto_model.goto_functions, - log.get_message_handler()); - goto_model.goto_functions.update(); - } + if(goto_model.can_produce_function(INITIALIZE_FUNCTION)) + recreate_initialize_function(goto_model, message_handler); } void is_fresh_baset::update_fn_call( diff --git a/src/goto-instrument/stack_depth.cpp b/src/goto-instrument/stack_depth.cpp index 4eb4565e416..b8affc60471 100644 --- a/src/goto-instrument/stack_depth.cpp +++ b/src/goto-instrument/stack_depth.cpp @@ -40,18 +40,8 @@ static symbol_exprt add_stack_depth_symbol( bool failed = goto_model.symbol_table.add(new_symbol); CHECK_RETURN(!failed); - if(goto_model.goto_functions.function_map.erase(INITIALIZE_FUNCTION) != 0) - { - static_lifetime_init( - goto_model.symbol_table, - goto_model.symbol_table.lookup_ref(INITIALIZE_FUNCTION).location); - goto_convert( - INITIALIZE_FUNCTION, - goto_model.symbol_table, - goto_model.goto_functions, - message_handler); - goto_model.goto_functions.update(); - } + if(goto_model.can_produce_function(INITIALIZE_FUNCTION)) + recreate_initialize_function(goto_model, message_handler); return new_symbol.symbol_expr(); } diff --git a/src/goto-programs/link_to_library.cpp b/src/goto-programs/link_to_library.cpp index 6c74ba18064..ed26d11a85b 100644 --- a/src/goto-programs/link_to_library.cpp +++ b/src/goto-programs/link_to_library.cpp @@ -159,19 +159,8 @@ void link_to_library( break; } - if(need_reinit) - { - goto_model.unload(INITIALIZE_FUNCTION); - static_lifetime_init( - goto_model.symbol_table, - goto_model.symbol_table.lookup_ref(INITIALIZE_FUNCTION).location); - goto_convert( - INITIALIZE_FUNCTION, - goto_model.symbol_table, - goto_model.goto_functions, - message_handler); - goto_model.goto_functions.update(); - } + if(need_reinit && goto_model.can_produce_function(INITIALIZE_FUNCTION)) + recreate_initialize_function(goto_model, message_handler); if(!object_type_updates.empty()) finalize_linking(goto_model, object_type_updates); diff --git a/src/goto-programs/slice_global_inits.cpp b/src/goto-programs/slice_global_inits.cpp index 5ef08988620..e006fa0c1c7 100644 --- a/src/goto-programs/slice_global_inits.cpp +++ b/src/goto-programs/slice_global_inits.cpp @@ -22,7 +22,6 @@ Date: December 2016 #include -#include "goto_convert_functions.h" #include "goto_functions.h" #include "goto_model.h" @@ -132,18 +131,6 @@ void slice_global_inits( } } - if( - changed && - goto_model.goto_functions.function_map.erase(INITIALIZE_FUNCTION) != 0) - { - static_lifetime_init( - goto_model.symbol_table, - goto_model.symbol_table.lookup_ref(INITIALIZE_FUNCTION).location); - goto_convert( - INITIALIZE_FUNCTION, - goto_model.symbol_table, - goto_model.goto_functions, - message_handler); - goto_model.goto_functions.update(); - } + if(changed && goto_model.can_produce_function(INITIALIZE_FUNCTION)) + recreate_initialize_function(goto_model, message_handler); } diff --git a/src/linking/CMakeLists.txt b/src/linking/CMakeLists.txt index 4534ff02476..885bfa15387 100644 --- a/src/linking/CMakeLists.txt +++ b/src/linking/CMakeLists.txt @@ -3,4 +3,4 @@ add_library(linking ${sources}) generic_includes(linking) -target_link_libraries(linking util) +target_link_libraries(linking goto-programs util) diff --git a/src/linking/static_lifetime_init.cpp b/src/linking/static_lifetime_init.cpp index d59a63e789d..ece82ad5507 100644 --- a/src/linking/static_lifetime_init.cpp +++ b/src/linking/static_lifetime_init.cpp @@ -16,6 +16,9 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include +#include + #include static optionalt static_lifetime_init( @@ -157,3 +160,21 @@ void static_lifetime_init( } } } + +void recreate_initialize_function( + goto_modelt &goto_model, + message_handlert &message_handler) +{ + auto unloaded = goto_model.unload(INITIALIZE_FUNCTION); + PRECONDITION(unloaded == 1); + + static_lifetime_init( + goto_model.symbol_table, + goto_model.symbol_table.lookup_ref(INITIALIZE_FUNCTION).location); + goto_convert( + INITIALIZE_FUNCTION, + goto_model.symbol_table, + goto_model.goto_functions, + message_handler); + goto_model.goto_functions.update(); +} diff --git a/src/linking/static_lifetime_init.h b/src/linking/static_lifetime_init.h index 84f5b77df98..40c2e856fea 100644 --- a/src/linking/static_lifetime_init.h +++ b/src/linking/static_lifetime_init.h @@ -12,6 +12,8 @@ Author: Daniel Kroening, kroening@kroening.com #include +class goto_modelt; +class message_handlert; class source_locationt; class symbol_table_baset; @@ -21,4 +23,9 @@ void static_lifetime_init( #define INITIALIZE_FUNCTION CPROVER_PREFIX "initialize" +/// Regenerates the CPROVER_INITIALIZE function, which initializes all +/// non-function symbols of the goto model that have static lifetime. It is an +/// error if CPROVER_INITIALIZE was not present beforehand. +void recreate_initialize_function(goto_modelt &, message_handlert &); + #endif // CPROVER_LINKING_STATIC_LIFETIME_INIT_H