Add a CL-specific message handler

console_message_handlert does not print source lines, which we do in GCC
mode and should also be doing in CL mode.

Author: tautschnig

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

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 const-array.c
  ^.*: .* is constant$
 ^   array\[1\] = 2;$

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

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 const-member.c
 
 ^.*: .* is constant$

src/goto-cc/Makefile

@@ -4,6 +4,7 @@ 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 \

src/goto-cc/cl_message_handler.cpp

@@ -0,0 +1,63 @@
+/*******************************************************************\
+
+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' << source_line;
+    }
+  }
+
+  console_message_handlert::print(level, formatted_message.str());
+}

src/goto-cc/cl_message_handler.h

@@ -0,0 +1,32 @@
+/*******************************************************************\
+
+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;
+};
+
+#endif // CPROVER_GOTO_CC_CL_MESSAGE_HANDLER_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