CL message handler

regression/ansi-c/const1/array-of-const.desc

@@ -1,6 +1,7 @@
 CORE
 array-of-const.c
- ^.*: .* is constant$
+
+^.*: .* is constant$
 ^EXIT=(1|64)$
 ^SIGNAL=0$
 --

regression/ansi-c/const1/const-array.desc

@@ -1,7 +1,8 @@
-KNOWNBUG
+CORE
 const-array.c
- ^.*: .* is constant$
-^   array\[1\] = 2;$
+
+^.*: .* is constant$
+array\[1\] = 2;$
 ^EXIT=(1|64)$
 ^SIGNAL=0$
 --

regression/ansi-c/const1/const-member.desc

@@ -1,8 +1,8 @@
-KNOWNBUG
+CORE
 const-member.c
 
 ^.*: .* is constant$
-^   const_struct_ptr->field = 123;$
+const_struct_ptr->field = 123;$
 ^EXIT=(1|64)$
 ^SIGNAL=0$
 --

src/goto-cc/Makefile

@@ -4,9 +4,11 @@ SRC = armcc_cmdline.cpp \
       as_cmdline.cpp \
       as_mode.cpp \
       bcc_cmdline.cpp \
+      cl_message_handler.cpp \
       compile.cpp \
       cw_mode.cpp \
       gcc_cmdline.cpp \
+      gcc_message_handler.cpp \
       gcc_mode.cpp \
       gcc_version.cpp \
       goto_cc_cmdline.cpp \

src/goto-cc/armcc_mode.h

@@ -14,10 +14,9 @@ Date: June 2006
 #ifndef CPROVER_GOTO_CC_ARMCC_MODE_H
 #define CPROVER_GOTO_CC_ARMCC_MODE_H
 
-#include <util/cout_message.h>
-
-#include "goto_cc_mode.h"
 #include "armcc_cmdline.h"
+#include "gcc_message_handler.h"
+#include "goto_cc_mode.h"
 
 class armcc_modet:public goto_cc_modet
 {

src/goto-cc/as_mode.cpp

@@ -24,7 +24,6 @@ Author: Michael Tautschnig
 #include <cstring>
 
 #include <util/config.h>
-#include <util/cout_message.h>
 #include <util/get_base_name.h>
 #include <util/run.h>
 #include <util/tempdir.h>

src/goto-cc/as_mode.h

@@ -14,8 +14,7 @@ Date: July 2016
 #ifndef CPROVER_GOTO_CC_AS_MODE_H
 #define CPROVER_GOTO_CC_AS_MODE_H
 
-#include <util/cout_message.h>
-
+#include "gcc_message_handler.h"
 #include "goto_cc_mode.h"
 
 class as_modet:public goto_cc_modet

src/goto-cc/cl_message_handler.cpp

@@ -0,0 +1,66 @@
+/*******************************************************************\
+
+Module: Print messages like CL.exe does
+
+Author: Michael Tautschnig
+
+\*******************************************************************/
+
+#include "cl_message_handler.h"
+
+#include <util/unicode.h>
+
+#include <fstream>
+#include <iostream>
+#include <sstream>
+
+void cl_message_handlert::print(
+  unsigned level,
+  const std::string &message,
+  const source_locationt &location)
+{
+  if(verbosity < level || location == source_locationt())
+  {
+    console_message_handlert::print(level, message);
+    return;
+  }
+
+  std::ostringstream formatted_message;
+
+  const irep_idt file = location.get_file();
+  const std::string &line = id2string(location.get_line());
+  formatted_message << file << '(' << line << "): ";
+
+  if(level == messaget::M_ERROR)
+    formatted_message << "error: ";
+  else if(level == messaget::M_WARNING)
+    formatted_message << "warning: ";
+
+  formatted_message << message;
+
+  const auto full_path = location.full_path();
+
+  if(full_path.has_value() && !line.empty())
+  {
+#ifdef _WIN32
+    std::ifstream in(widen(full_path.value()));
+#else
+    std::ifstream in(full_path.value());
+#endif
+    if(in)
+    {
+      const auto line_number = std::stoull(line);
+      std::string source_line;
+      for(std::size_t l = 0; l < line_number; l++)
+        std::getline(in, source_line);
+
+      if(in)
+      {
+        formatted_message << '\n';
+        formatted_message << file << '(' << line << "): " << source_line;
+      }
+    }
+  }
+
+  console_message_handlert::print(level, formatted_message.str());
+}

src/goto-cc/cl_message_handler.h

@@ -0,0 +1,34 @@
+/*******************************************************************\
+
+Module: Print messages like CL.exe does
+
+Author: Michael Tautschnig
+
+\*******************************************************************/
+
+#ifndef CPROVER_GOTO_CC_CL_MESSAGE_HANDLER_H
+#define CPROVER_GOTO_CC_CL_MESSAGE_HANDLER_H
+
+#include <util/cout_message.h>
+
+class cl_message_handlert : public console_message_handlert
+{
+public:
+  void print(unsigned, const xmlt &) override
+  {
+  }
+
+  void print(unsigned, const jsont &) override
+  {
+  }
+
+  // aims to imitate the messages CL prints
+  void print(
+    unsigned level,
+    const std::string &message,
+    const source_locationt &location) override;
+
+  using console_message_handlert::print;
+};
+
+#endif // CPROVER_GOTO_CC_CL_MESSAGE_HANDLER_H

src/goto-cc/gcc_message_handler.cpp

@@ -0,0 +1,97 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#include "gcc_message_handler.h"
+
+#include <util/unicode.h>
+
+#include <fstream>
+#include <iostream>
+
+void gcc_message_handlert::print(
+  unsigned level,
+  const std::string &message,
+  const source_locationt &location)
+{
+  message_handlert::print(level, message);
+
+  if(verbosity >= level)
+  {
+    // gcc appears to send everything to cerr
+    auto &out = std::cerr;
+
+    const irep_idt file = location.get_file();
+    const irep_idt line = location.get_line();
+    const irep_idt column = location.get_column();
+    const irep_idt function = location.get_function();
+
+    if(!function.empty())
+    {
+      if(!file.empty())
+        out << string(messaget::bold) << file << ':' << string(messaget::reset)
+            << ' ';
+      out << "In function " << string(messaget::bold) << '\'' << function
+          << '\'' << string(messaget::reset) << ":\n";
+    }
+
+    if(!line.empty())
+    {
+      out << string(messaget::bold);
+
+      if(!file.empty())
+        out << file << ':';
+
+      out << line << ':';
+
+      if(column.empty())
+        out << "1: ";
+      else
+        out << column << ": ";
+
+      if(level == messaget::M_ERROR)
+        out << string(messaget::red) << "error: ";
+      else if(level == messaget::M_WARNING)
+        out << string(messaget::bright_magenta) << "warning: ";
+
+      out << string(messaget::reset);
+    }
+
+    out << message << '\n';
+
+    const auto file_name = location.full_path();
+    if(file_name.has_value() && !line.empty())
+    {
+#ifdef _WIN32
+      std::ifstream in(widen(file_name.value()));
+#else
+      std::ifstream in(file_name.value());
+#endif
+      if(in)
+      {
+        const auto line_number = std::stoull(id2string(line));
+        std::string source_line;
+        for(std::size_t l = 0; l < line_number; l++)
+          std::getline(in, source_line);
+
+        if(in)
+          out << ' ' << source_line << '\n'; // gcc adds a space, clang doesn't
+      }
+    }
+
+    out << std::flush;
+  }
+}
+
+void gcc_message_handlert::print(unsigned level, const std::string &message)
+{
+  message_handlert::print(level, message);
+
+  // gcc appears to send everything to cerr
+  if(verbosity >= level)
+    std::cerr << message << '\n' << std::flush;
+}

src/goto-cc/gcc_message_handler.h

@@ -0,0 +1,41 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#ifndef CPROVER_GOTO_CC_GCC_MESSAGE_HANDLER_H
+#define CPROVER_GOTO_CC_GCC_MESSAGE_HANDLER_H
+
+#include <util/cout_message.h>
+
+class gcc_message_handlert : public console_message_handlert
+{
+public:
+  void print(unsigned, const xmlt &) override
+  {
+  }
+
+  void print(unsigned, const jsont &) override
+  {
+  }
+
+  // aims to imitate the messages gcc prints
+  void print(unsigned level, const std::string &message) override;
+
+  void print(
+    unsigned level,
+    const std::string &message,
+    const source_locationt &location) override;
+
+private:
+  /// feed a command into a string
+  std::string string(const messaget::commandt &c) const
+  {
+    return command(c.command);
+  }
+};
+
+#endif // CPROVER_GOTO_CC_GCC_MESSAGE_HANDLER_H

src/goto-cc/gcc_mode.h

@@ -15,11 +15,10 @@ Date: June 2006
 #define CPROVER_GOTO_CC_GCC_MODE_H
 
 #include "compile.h"
+#include "gcc_message_handler.h"
 #include "gcc_version.h"
 #include "goto_cc_mode.h"
 
-#include <util/cout_message.h>
-
 #include <set>
 
 class gcc_modet:public goto_cc_modet

src/goto-cc/ld_mode.h

@@ -15,10 +15,9 @@ Date: June 2006
 #define CPROVER_GOTO_CC_LD_MODE_H
 
 #include "compile.h"
+#include "gcc_message_handler.h"
 #include "goto_cc_mode.h"
 
-#include <util/cout_message.h>
-
 #include <set>
 
 class ld_modet : public goto_cc_modet

src/goto-cc/linker_script_merge.h

@@ -7,7 +7,6 @@
 
 #include <functional>
 
-#include <util/cout_message.h>
 #include <util/json.h>
 
 #include "compile.h"

src/goto-cc/ms_cl_mode.h

@@ -14,8 +14,7 @@ Date: June 2006
 #ifndef CPROVER_GOTO_CC_MS_CL_MODE_H
 #define CPROVER_GOTO_CC_MS_CL_MODE_H
 
-#include <util/cout_message.h>
-
+#include "cl_message_handler.h"
 #include "goto_cc_mode.h"
 #include "ms_cl_cmdline.h"
 
@@ -35,7 +34,7 @@ class ms_cl_modet:public goto_cc_modet
 
 protected:
   ms_cl_cmdlinet &cmdline;
-  console_message_handlert message_handler;
+  cl_message_handlert message_handler;
 };
 
 #endif // CPROVER_GOTO_CC_MS_CL_MODE_H

src/goto-cc/ms_link_mode.h

@@ -14,11 +14,10 @@ Date: July 2018
 #ifndef CPROVER_GOTO_CC_MS_LINK_MODE_H
 #define CPROVER_GOTO_CC_MS_LINK_MODE_H
 
+#include "cl_message_handler.h"
 #include "compile.h"
 #include "goto_cc_mode.h"
 
-#include <util/cout_message.h>
-
 class ms_link_modet : public goto_cc_modet
 {
 public:
@@ -28,7 +27,7 @@ class ms_link_modet : public goto_cc_modet
   explicit ms_link_modet(goto_cc_cmdlinet &);
 
 protected:
-  console_message_handlert message_handler;
+  cl_message_handlert message_handler;
 };
 
 #endif // CPROVER_GOTO_CC_MS_LINK_MODE_H