From 1bc815feae58abf9700a592752bdd4f6cc493c2d Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 21 Apr 2023 12:40:44 +0000 Subject: [PATCH] Make goto_{model,functions}t::unload return a value This will enable its use in place of .erase(...) when such a call required the number of functions that had been removed. The key user will be a refactored initialize-function re-creation code. --- jbmc/src/java_bytecode/lazy_goto_functions_map.h | 7 +++++-- jbmc/src/java_bytecode/lazy_goto_model.cpp | 2 +- src/goto-programs/goto_functions.h | 9 +++++++-- src/goto-programs/goto_model.h | 8 +++++++- src/goto-programs/initialize_goto_model.cpp | 4 ++-- src/goto-programs/initialize_goto_model.h | 2 +- 6 files changed, 23 insertions(+), 9 deletions(-) diff --git a/jbmc/src/java_bytecode/lazy_goto_functions_map.h b/jbmc/src/java_bytecode/lazy_goto_functions_map.h index d8af53dc9b5..aaff168b2a6 100644 --- a/jbmc/src/java_bytecode/lazy_goto_functions_map.h +++ b/jbmc/src/java_bytecode/lazy_goto_functions_map.h @@ -126,9 +126,12 @@ class lazy_goto_functions_mapt final driver_program_can_generate_function_body(name); } - void unload(const key_type &name) const + /// Remove the function named \p name from the function map, if it exists. + /// \return Returns 0 when \p name was not present, and 1 when \p name was + /// removed. + std::size_t unload(const key_type &name) const { - goto_functions.erase(name); + return goto_functions.erase(name); } void ensure_function_loaded(const key_type &name) const diff --git a/jbmc/src/java_bytecode/lazy_goto_model.cpp b/jbmc/src/java_bytecode/lazy_goto_model.cpp index 0252346c1dd..c3a183d74fe 100644 --- a/jbmc/src/java_bytecode/lazy_goto_model.cpp +++ b/jbmc/src/java_bytecode/lazy_goto_model.cpp @@ -170,7 +170,7 @@ void lazy_goto_modelt::initialize( set_up_custom_entry_point( language_files, symbol_table, - [this](const irep_idt &id) { goto_functions.unload(id); }, + [this](const irep_idt &id) { return goto_functions.unload(id); }, options, false, message_handler); diff --git a/src/goto-programs/goto_functions.h b/src/goto-programs/goto_functions.h index 01a73e7e625..73f8d06ba1d 100644 --- a/src/goto-programs/goto_functions.h +++ b/src/goto-programs/goto_functions.h @@ -66,8 +66,13 @@ class goto_functionst return *this; } - /// Remove function from the function map - void unload(const irep_idt &name) { function_map.erase(name); } + /// Remove the function named \p name from the function map, if it exists. + /// \return Returns 0 when \p name was not present, and 1 when \p name was + /// removed. + std::size_t unload(const irep_idt &name) + { + return function_map.erase(name); + } void clear() { diff --git a/src/goto-programs/goto_model.h b/src/goto-programs/goto_model.h index b5e0c55a839..7debed5795c 100644 --- a/src/goto-programs/goto_model.h +++ b/src/goto-programs/goto_model.h @@ -66,7 +66,13 @@ class goto_modelt : public abstract_goto_modelt return *this; } - void unload(const irep_idt &name) { goto_functions.unload(name); } + /// Remove the function named \p name from the function map, if it exists. + /// \return Returns 0 when \p name was not present, and 1 when \p name was + /// removed. + std::size_t unload(const irep_idt &name) + { + return goto_functions.unload(name); + } // Implement the abstract goto model interface: diff --git a/src/goto-programs/initialize_goto_model.cpp b/src/goto-programs/initialize_goto_model.cpp index 840241c59b5..20e1ada9e8a 100644 --- a/src/goto-programs/initialize_goto_model.cpp +++ b/src/goto-programs/initialize_goto_model.cpp @@ -120,7 +120,7 @@ void initialize_from_source_files( void set_up_custom_entry_point( language_filest &language_files, symbol_tablet &symbol_table, - const std::function &unload, + const std::function &unload, const optionst &options, bool try_mode_lookup, message_handlert &message_handler) @@ -213,7 +213,7 @@ goto_modelt initialize_goto_model( set_up_custom_entry_point( language_files, goto_model.symbol_table, - [&goto_model](const irep_idt &id) { goto_model.goto_functions.unload(id); }, + [&goto_model](const irep_idt &id) { return goto_model.unload(id); }, options, true, message_handler); diff --git a/src/goto-programs/initialize_goto_model.h b/src/goto-programs/initialize_goto_model.h index e0cb1f23112..6925a10e3f5 100644 --- a/src/goto-programs/initialize_goto_model.h +++ b/src/goto-programs/initialize_goto_model.h @@ -51,7 +51,7 @@ void initialize_from_source_files( void set_up_custom_entry_point( language_filest &language_files, symbol_tablet &symbol_table, - const std::function &unload, + const std::function &unload, const optionst &options, bool try_mode_lookup, message_handlert &message_handler);