Skip to content

Commit 1bc815f

Browse files
committed
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.
1 parent f39a5c1 commit 1bc815f

File tree

6 files changed

+23
-9
lines changed

6 files changed

+23
-9
lines changed

jbmc/src/java_bytecode/lazy_goto_functions_map.h

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -126,9 +126,12 @@ class lazy_goto_functions_mapt final
126126
driver_program_can_generate_function_body(name);
127127
}
128128

129-
void unload(const key_type &name) const
129+
/// Remove the function named \p name from the function map, if it exists.
130+
/// \return Returns 0 when \p name was not present, and 1 when \p name was
131+
/// removed.
132+
std::size_t unload(const key_type &name) const
130133
{
131-
goto_functions.erase(name);
134+
return goto_functions.erase(name);
132135
}
133136

134137
void ensure_function_loaded(const key_type &name) const

jbmc/src/java_bytecode/lazy_goto_model.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -170,7 +170,7 @@ void lazy_goto_modelt::initialize(
170170
set_up_custom_entry_point(
171171
language_files,
172172
symbol_table,
173-
[this](const irep_idt &id) { goto_functions.unload(id); },
173+
[this](const irep_idt &id) { return goto_functions.unload(id); },
174174
options,
175175
false,
176176
message_handler);

src/goto-programs/goto_functions.h

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -66,8 +66,13 @@ class goto_functionst
6666
return *this;
6767
}
6868

69-
/// Remove function from the function map
70-
void unload(const irep_idt &name) { function_map.erase(name); }
69+
/// Remove the function named \p name from the function map, if it exists.
70+
/// \return Returns 0 when \p name was not present, and 1 when \p name was
71+
/// removed.
72+
std::size_t unload(const irep_idt &name)
73+
{
74+
return function_map.erase(name);
75+
}
7176

7277
void clear()
7378
{

src/goto-programs/goto_model.h

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -66,7 +66,13 @@ class goto_modelt : public abstract_goto_modelt
6666
return *this;
6767
}
6868

69-
void unload(const irep_idt &name) { goto_functions.unload(name); }
69+
/// Remove the function named \p name from the function map, if it exists.
70+
/// \return Returns 0 when \p name was not present, and 1 when \p name was
71+
/// removed.
72+
std::size_t unload(const irep_idt &name)
73+
{
74+
return goto_functions.unload(name);
75+
}
7076

7177
// Implement the abstract goto model interface:
7278

src/goto-programs/initialize_goto_model.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -120,7 +120,7 @@ void initialize_from_source_files(
120120
void set_up_custom_entry_point(
121121
language_filest &language_files,
122122
symbol_tablet &symbol_table,
123-
const std::function<void(const irep_idt &)> &unload,
123+
const std::function<std::size_t(const irep_idt &)> &unload,
124124
const optionst &options,
125125
bool try_mode_lookup,
126126
message_handlert &message_handler)
@@ -213,7 +213,7 @@ goto_modelt initialize_goto_model(
213213
set_up_custom_entry_point(
214214
language_files,
215215
goto_model.symbol_table,
216-
[&goto_model](const irep_idt &id) { goto_model.goto_functions.unload(id); },
216+
[&goto_model](const irep_idt &id) { return goto_model.unload(id); },
217217
options,
218218
true,
219219
message_handler);

src/goto-programs/initialize_goto_model.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -51,7 +51,7 @@ void initialize_from_source_files(
5151
void set_up_custom_entry_point(
5252
language_filest &language_files,
5353
symbol_tablet &symbol_table,
54-
const std::function<void(const irep_idt &)> &unload,
54+
const std::function<std::size_t(const irep_idt &)> &unload,
5555
const optionst &options,
5656
bool try_mode_lookup,
5757
message_handlert &message_handler);

0 commit comments

Comments
 (0)