Merge pull request #7678 from tautschnig/features/unload

Make goto_{model,functions}t::unload return a value

Author: tautschnig

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

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);

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()
   {

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:
 

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<void(const irep_idt &)> &unload,
+  const std::function<std::size_t(const irep_idt &)> &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);

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<void(const irep_idt &)> &unload,
+  const std::function<std::size_t(const irep_idt &)> &unload,
   const optionst &options,
   bool try_mode_lookup,
   message_handlert &message_handler);