Skip to content

Pass a message handler to is_goto_binary [blocks: #3867] #4341

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.

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
Mar 7, 2019
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
5 changes: 3 additions & 2 deletions src/cbmc/cbmc_parse_options.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -485,8 +485,9 @@ int cbmc_parse_optionst::doit()

if(cmdline.isset("show-parse-tree"))
{
if(cmdline.args.size()!=1 ||
is_goto_binary(cmdline.args[0]))
if(
cmdline.args.size() != 1 ||
is_goto_binary(cmdline.args[0], ui_message_handler))
{
error() << "Please give exactly one source file" << eom;
return CPROVER_EXIT_INCORRECT_TASK;
Expand Down
12 changes: 7 additions & 5 deletions src/goto-cc/compile.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -126,7 +126,9 @@ enum class file_typet
ELF_OBJECT
};

static file_typet detect_file_type(const std::string &file_name)
static file_typet detect_file_type(
const std::string &file_name,
message_handlert &message_handler)
{
// first of all, try to open the file
std::ifstream in(file_name);
Expand Down Expand Up @@ -154,7 +156,7 @@ static file_typet detect_file_type(const std::string &file_name)
if(ext == "a")
return file_typet::NORMAL_ARCHIVE;

if(is_goto_binary(file_name))
if(is_goto_binary(file_name, message_handler))
return file_typet::GOTO_BINARY;

if(hdr[0] == 0x7f && memcmp(hdr + 1, "ELF", 3) == 0)
Expand All @@ -167,7 +169,7 @@ static file_typet detect_file_type(const std::string &file_name)
/// \return false on success, true on error.
bool compilet::add_input_file(const std::string &file_name)
{
switch(detect_file_type(file_name))
switch(detect_file_type(file_name, get_message_handler()))
{
case file_typet::FAILED_TO_OPEN_FILE:
warning() << "failed to open file `" << file_name
Expand Down Expand Up @@ -249,7 +251,7 @@ bool compilet::add_files_from_archive(
{
std::string t = concat_dir_file(tstr, line);

if(is_goto_binary(t))
if(is_goto_binary(t, get_message_handler()))
object_files.push_back(t);
else
debug() << "Object file is not a goto binary: " << line << eom;
Expand Down Expand Up @@ -280,7 +282,7 @@ bool compilet::find_library(const std::string &name)
{
library_file_name = concat_dir_file(library_path, "lib" + name + ".so");

switch(detect_file_type(library_file_name))
switch(detect_file_type(library_file_name, get_message_handler()))
{
case file_typet::GOTO_BINARY:
return !add_input_file(library_file_name);
Expand Down
2 changes: 1 addition & 1 deletion src/goto-programs/initialize_goto_model.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -75,7 +75,7 @@ goto_modelt initialize_goto_model(

for(const auto &file : files)
{
if(is_goto_binary(file))
if(is_goto_binary(file, message_handler))
binaries.push_back(file);
else
sources.push_back(file);
Expand Down
2 changes: 1 addition & 1 deletion src/goto-programs/lazy_goto_model.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -128,7 +128,7 @@ void lazy_goto_modelt::initialize(

for(const auto &file : files)
{
if(is_goto_binary(file))
if(is_goto_binary(file, message_handler))
binaries.push_back(file);
else
sources.push_back(file);
Expand Down
2 changes: 1 addition & 1 deletion src/goto-programs/read_goto_binary.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -155,7 +155,7 @@ static bool read_goto_binary(
return true;
}

bool is_goto_binary(const std::string &filename)
bool is_goto_binary(const std::string &filename, message_handlert &)
{
#ifdef _MSC_VER
std::ifstream in(widen(filename), std::ios::binary);
Expand Down
2 changes: 1 addition & 1 deletion src/goto-programs/read_goto_binary.h
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@ class symbol_tablet;
optionalt<goto_modelt>
read_goto_binary(const std::string &filename, message_handlert &);

bool is_goto_binary(const std::string &filename);
bool is_goto_binary(const std::string &filename, message_handlert &);

bool read_object_and_link(
const std::string &file_name,
Expand Down