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,51 @@
+/*******************************************************************\
+
+Module: Print messages like CL.exe does
+
+Author: Michael Tautschnig
+
+\*******************************************************************/
+
+#include "cl_message_handler.h"
+
+#include <fstream>
+#include <iostream>
+
+#include "unicode.h"
+
+void console_message_handlert::print(
+  unsigned level,
+  const std::string &message,
+  const source_locationt &location)
+{
+  console_message_handlert::print(level, message, location);
+
+  const auto file_name = location.full_path();
+  const std::string &line = id2string(location.get_line());
+
+  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(line);
+      std::string source_line;
+      for(std::size_t l = 0; l < line_number; l++)
+        std::getline(in, source_line);
+
+      if(in)
+      {
+        // Messages level 3 or lower go to cerr, messages level 4 or
+        // above go to cout.
+        if(level>=4)
+          std::cout << ' ' << source_line << '\n';
+        else
+          std::cerr << ' ' << source_line << '\n';
+      }
+    }
+  }
+}

src/goto-cc/cl_message_handler.h

@@ -0,0 +1,23 @@
+/*******************************************************************\
+
+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 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