From a3afbcf5020a6dda1a3a2f0200083f38f462e14d Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 22 Jan 2019 13:28:30 +0000 Subject: [PATCH] Pass a message handler to is_goto_binary This is in preparation of support for goto-cc sections in OS X Mach-O files, where we will want to report problems while attempting to read a file. --- src/cbmc/cbmc_parse_options.cpp | 5 +++-- src/goto-cc/compile.cpp | 12 +++++++----- src/goto-programs/initialize_goto_model.cpp | 2 +- src/goto-programs/lazy_goto_model.cpp | 2 +- src/goto-programs/read_goto_binary.cpp | 2 +- src/goto-programs/read_goto_binary.h | 2 +- 6 files changed, 14 insertions(+), 11 deletions(-) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index aa68f37ef8a..22e3a67aaac 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -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; diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp index fa29a36bdf8..0d21575bc63 100644 --- a/src/goto-cc/compile.cpp +++ b/src/goto-cc/compile.cpp @@ -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); @@ -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) @@ -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 @@ -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; @@ -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); diff --git a/src/goto-programs/initialize_goto_model.cpp b/src/goto-programs/initialize_goto_model.cpp index 67d291631c6..190133c1541 100644 --- a/src/goto-programs/initialize_goto_model.cpp +++ b/src/goto-programs/initialize_goto_model.cpp @@ -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); diff --git a/src/goto-programs/lazy_goto_model.cpp b/src/goto-programs/lazy_goto_model.cpp index 526882452f6..4884e27d571 100644 --- a/src/goto-programs/lazy_goto_model.cpp +++ b/src/goto-programs/lazy_goto_model.cpp @@ -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); diff --git a/src/goto-programs/read_goto_binary.cpp b/src/goto-programs/read_goto_binary.cpp index 25646163cb0..82650552c20 100644 --- a/src/goto-programs/read_goto_binary.cpp +++ b/src/goto-programs/read_goto_binary.cpp @@ -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); diff --git a/src/goto-programs/read_goto_binary.h b/src/goto-programs/read_goto_binary.h index 7487119a250..2ed05a37dfe 100644 --- a/src/goto-programs/read_goto_binary.h +++ b/src/goto-programs/read_goto_binary.h @@ -25,7 +25,7 @@ class symbol_tablet; optionalt 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,