Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
May 5, 2023
Merged

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

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 5 additions & 2 deletions jbmc/src/java_bytecode/lazy_goto_functions_map.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is using std::size_t for this purpose a thing?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Would you recommend using underlying_mapt::size_type instead? That's the exact return type of erase, but I'd expect it to be std::size_t on all platforms.

{
goto_functions.erase(name);
return goto_functions.erase(name);
}

void ensure_function_loaded(const key_type &name) const
Expand Down
2 changes: 1 addition & 1 deletion jbmc/src/java_bytecode/lazy_goto_model.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down
9 changes: 7 additions & 2 deletions src/goto-programs/goto_functions.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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()
{
Expand Down
8 changes: 7 additions & 1 deletion src/goto-programs/goto_model.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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:

Expand Down
4 changes: 2 additions & 2 deletions src/goto-programs/initialize_goto_model.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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);
Expand Down
2 changes: 1 addition & 1 deletion src/goto-programs/initialize_goto_model.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down