Merge pull request #4341 from tautschnig/is_goto_binary

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

Author: tautschnig

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;

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);

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);

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);

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);

src/goto-programs/read_goto_binary.h

@@ -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,