Skip to content

JBMC: Remove-returns per function #1730

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 2 commits into from
Jan 23, 2018
Merged

JBMC: Remove-returns per function #1730

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
a7595c1
Remove returns: support running per-function
smowton Jan 11, 2018
96569c3
JBMC: remove return values on a per-function basis
smowton Jan 12, 2018
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
0 regression/cbmc-java/exceptions25/main.c → ...cbmc/uncaught_exceptions_analysis1/main.c
View file
Open in desktop
File renamed without changes.
0 regression/cbmc-java/exceptions25/test.desc → ...c/uncaught_exceptions_analysis1/test.desc
View file
Open in desktop
File renamed without changes.
10 changes: 10 additions & 0 deletions src/goto-programs/lazy_goto_functions_map.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -99,6 +99,16 @@ class lazy_goto_functions_mapt final
return ensure_function_loaded_internal(name).second;
}

/// Determines if this lazy GOTO functions map can produce a body for the
/// given function
/// \param name: function ID to query
/// \return true if we can produce a function body, or false if we would leave
/// it a bodyless stub.
bool can_produce_function(const key_type &name) const
{
return language_files.can_convert_lazy_method(name);
}

void unload(const key_type &name) const { goto_functions.erase(name); }

void ensure_function_loaded(const key_type &name) const
Expand Down
9 changes: 7 additions & 2 deletions src/goto-programs/lazy_goto_model.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ lazy_goto_modelt::lazy_goto_modelt(
[this] (goto_functionst::goto_functiont &function) -> void
{
goto_model_functiont model_function(*goto_model, function);
this->post_process_function(model_function);
this->post_process_function(model_function, *this);
},
message_handler),
post_process_function(std::move(post_process_function)),
Expand All @@ -51,7 +51,7 @@ lazy_goto_modelt::lazy_goto_modelt(lazy_goto_modelt &&other)
[this] (goto_functionst::goto_functiont &function) -> void
{
goto_model_functiont model_function(*goto_model, function);
this->post_process_function(model_function);
this->post_process_function(model_function, *this);
},
other.message_handler),
language_files(std::move(other.language_files)),
Expand Down Expand Up @@ -239,3 +239,8 @@ bool lazy_goto_modelt::finalize()

return post_process_functions(*goto_model);
}

bool lazy_goto_modelt::can_produce_function(const irep_idt &id) const
{
return goto_functions.can_produce_function(id);
}
27 changes: 20 additions & 7 deletions src/goto-programs/lazy_goto_model.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,11 +15,24 @@
class cmdlinet;
class optionst;

/// Interface for a provider of function definitions to report whether or not it
/// can provide a definition (function body) for a given function ID.
struct can_produce_functiont
{
/// Determines if this function provider can produce a body for the given
/// function
/// \param id: function ID to query
/// \return true if we can produce a function body, or false if we would leave
/// it a bodyless stub.
virtual bool can_produce_function(const irep_idt &id) const = 0;
};

/// Model that holds partially loaded map of functions
class lazy_goto_modelt
class lazy_goto_modelt : public can_produce_functiont
Copy link
Collaborator

Choose a reason for hiding this comment

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

I don't know what a can_produce_functiont is supposed to be, hence I can't judge whether this is-a relation is justified.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

See new docs on the interface

Copy link
Collaborator

Choose a reason for hiding this comment

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

Thanks a lot for the clarification!

{
public:
typedef std::function<void(goto_model_functiont &function)>
typedef std::function<
void(goto_model_functiont &function, const can_produce_functiont &)>
post_process_functiont;
typedef std::function<bool(goto_modelt &goto_model)> post_process_functionst;

Expand Down Expand Up @@ -51,12 +64,10 @@ class lazy_goto_modelt
message_handlert &message_handler)
{
return lazy_goto_modelt(
[&handler] (goto_model_functiont &function)
{
handler.process_goto_function(function);
[&handler] (goto_model_functiont &fun, const can_produce_functiont &cpf) { // NOLINT(*)
handler.process_goto_function(fun, cpf);
},
[&handler, &options] (goto_modelt &goto_model) -> bool
{
[&handler, &options] (goto_modelt &goto_model) -> bool { // NOLINT(*)
return handler.process_goto_functions(goto_model, options);
},
message_handler);
Expand Down Expand Up @@ -88,6 +99,8 @@ class lazy_goto_modelt
return std::move(model.goto_model);
}

virtual bool can_produce_function(const irep_idt &id) const;

private:
std::unique_ptr<goto_modelt> goto_model;

Expand Down
Loading