diff --git a/src/goto-cc/armcc_mode.cpp b/src/goto-cc/armcc_mode.cpp
index fbe8db16d94..f4a57655582 100644
--- a/src/goto-cc/armcc_mode.cpp
+++ b/src/goto-cc/armcc_mode.cpp
@@ -59,8 +59,8 @@ int armcc_modet::doit()
   if(cmdline.isset("verbosity"))
     verbosity=unsafe_string2int(cmdline.get_value("verbosity"));
 
-  compiler.ui_message_handler.set_verbosity(verbosity);
-  ui_message_handler.set_verbosity(verbosity);
+  compiler.set_message_handler(get_message_handler());
+  message_handler.set_verbosity(verbosity);
 
   debug() << "ARM mode" << eom;
 
diff --git a/src/goto-cc/armcc_mode.h b/src/goto-cc/armcc_mode.h
index bf1481c8141..cbbe90a2a1e 100644
--- a/src/goto-cc/armcc_mode.h
+++ b/src/goto-cc/armcc_mode.h
@@ -11,25 +11,28 @@ 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"
 
 class armcc_modet:public goto_cc_modet
 {
 public:
-  virtual int doit();
-  virtual void help_mode();
+  int doit() final;
+  void help_mode() final;
 
   armcc_modet(
     armcc_cmdlinet &_armcc_cmdline,
     const std::string &_base_name):
-    goto_cc_modet(_armcc_cmdline, _base_name),
+    goto_cc_modet(_armcc_cmdline, _base_name, message_handler),
     cmdline(_armcc_cmdline)
   {
   }
 
 protected:
   armcc_cmdlinet &cmdline;
+  gcc_message_handlert message_handler;
 };
 
 #endif // CPROVER_GOTO_CC_ARMCC_MODE_H
diff --git a/src/goto-cc/as_mode.cpp b/src/goto-cc/as_mode.cpp
index 75d02f2903f..bb87b6c6abb 100644
--- a/src/goto-cc/as_mode.cpp
+++ b/src/goto-cc/as_mode.cpp
@@ -22,6 +22,7 @@ Author: Michael Tautschnig
 #include <util/tempdir.h>
 #include <util/config.h>
 #include <util/get_base_name.h>
+#include <util/cout_message.h>
 
 #include <cbmc/version.h>
 
@@ -79,7 +80,7 @@ as_modet::as_modet(
   goto_cc_cmdlinet &_cmdline,
   const std::string &_base_name,
   bool _produce_hybrid_binary):
-  goto_cc_modet(_cmdline, _base_name),
+  goto_cc_modet(_cmdline, _base_name, message_handler),
   produce_hybrid_binary(_produce_hybrid_binary),
   native_tool_name(assembler_name(cmdline, base_name))
 {
@@ -137,7 +138,7 @@ int as_modet::doit()
   if(cmdline.isset("verbosity"))
     verbosity=unsafe_string2unsigned(cmdline.get_value("verbosity"));
 
-  ui_message_handler.set_verbosity(verbosity);
+  message_handler.set_verbosity(verbosity);
 
   if(act_as_as86)
   {
diff --git a/src/goto-cc/as_mode.h b/src/goto-cc/as_mode.h
index 8b44800420e..04ad255a764 100644
--- a/src/goto-cc/as_mode.h
+++ b/src/goto-cc/as_mode.h
@@ -11,6 +11,8 @@ Date: July 2016
 #ifndef CPROVER_GOTO_CC_AS_MODE_H
 #define CPROVER_GOTO_CC_AS_MODE_H
 
+#include <util/cout_message.h>
+
 #include "goto_cc_mode.h"
 
 class as_modet:public goto_cc_modet
@@ -22,10 +24,11 @@ class as_modet:public goto_cc_modet
   as_modet(
     goto_cc_cmdlinet &_cmdline,
     const std::string &_base_name,
-    bool _produce_hybrid_binar);
+    bool _produce_hybrid_binary);
 
 protected:
-  bool produce_hybrid_binary;
+  gcc_message_handlert message_handler;
+  const bool produce_hybrid_binary;
   const std::string native_tool_name;
 
   int run_as(); // call as with original command line
diff --git a/src/goto-cc/cw_mode.cpp b/src/goto-cc/cw_mode.cpp
index a3a085d843c..510f7c9c0aa 100644
--- a/src/goto-cc/cw_mode.cpp
+++ b/src/goto-cc/cw_mode.cpp
@@ -59,8 +59,8 @@ int cw_modet::doit()
   if(cmdline.isset("verbosity"))
     verbosity=unsafe_string2unsigned(cmdline.get_value("verbosity"));
 
-  compiler.ui_message_handler.set_verbosity(verbosity);
-  ui_message_handler.set_verbosity(verbosity);
+  compiler.set_message_handler(get_message_handler());
+  message_handler.set_verbosity(verbosity);
 
   debug() << "CodeWarrior mode" << eom;
 
diff --git a/src/goto-cc/cw_mode.h b/src/goto-cc/cw_mode.h
index e81469e9460..865b1f7ea15 100644
--- a/src/goto-cc/cw_mode.h
+++ b/src/goto-cc/cw_mode.h
@@ -11,6 +11,8 @@ Date: June 2006
 #ifndef CPROVER_GOTO_CC_CW_MODE_H
 #define CPROVER_GOTO_CC_CW_MODE_H
 
+#include <util/cout_message.h>
+
 #include "goto_cc_mode.h"
 #include "gcc_cmdline.h"
 
@@ -21,13 +23,14 @@ class cw_modet:public goto_cc_modet
   virtual void help_mode();
 
   cw_modet(gcc_cmdlinet &_gcc_cmdline, const std::string &_base_name):
-    goto_cc_modet(_gcc_cmdline, _base_name),
+    goto_cc_modet(_gcc_cmdline, _base_name, message_handler),
     cmdline(_gcc_cmdline)
   {
   }
 
 protected:
   gcc_cmdlinet &cmdline;
+  console_message_handlert message_handler;
 };
 
 #endif // CPROVER_GOTO_CC_CW_MODE_H
diff --git a/src/goto-cc/gcc_mode.cpp b/src/goto-cc/gcc_mode.cpp
index 1762a4bc6a2..d56b2c3c351 100644
--- a/src/goto-cc/gcc_mode.cpp
+++ b/src/goto-cc/gcc_mode.cpp
@@ -121,7 +121,7 @@ gcc_modet::gcc_modet(
   goto_cc_cmdlinet &_cmdline,
   const std::string &_base_name,
   bool _produce_hybrid_binary):
-  goto_cc_modet(_cmdline, _base_name),
+  goto_cc_modet(_cmdline, _base_name, gcc_message_handler),
   produce_hybrid_binary(_produce_hybrid_binary),
   act_as_ld(base_name=="ld" ||
             base_name.find("goto-ld")!=std::string::npos)
@@ -223,7 +223,7 @@ int gcc_modet::doit()
   if(cmdline.isset("verbosity"))
     verbosity=unsafe_string2unsigned(cmdline.get_value("verbosity"));
 
-  ui_message_handler.set_verbosity(verbosity);
+  gcc_message_handler.set_verbosity(verbosity);
 
   if(act_as_ld)
   {
@@ -303,7 +303,7 @@ int gcc_modet::doit()
 
   // determine actions to be undertaken
   compilet compiler(cmdline);
-  compiler.ui_message_handler.set_verbosity(verbosity);
+  compiler.set_message_handler(get_message_handler());
 
   if(act_as_ld)
     compiler.mode=compilet::LINK_LIBRARY;
diff --git a/src/goto-cc/gcc_mode.h b/src/goto-cc/gcc_mode.h
index 669c140a45e..b15777e8fe9 100644
--- a/src/goto-cc/gcc_mode.h
+++ b/src/goto-cc/gcc_mode.h
@@ -11,13 +11,15 @@ Date: June 2006
 #ifndef CPROVER_GOTO_CC_GCC_MODE_H
 #define CPROVER_GOTO_CC_GCC_MODE_H
 
+#include <util/cout_message.h>
+
 #include "goto_cc_mode.h"
 
 class gcc_modet:public goto_cc_modet
 {
 public:
-  virtual int doit();
-  virtual void help_mode();
+  int doit() final;
+  void help_mode() final;
 
   gcc_modet(
     goto_cc_cmdlinet &_cmdline,
@@ -25,11 +27,13 @@ class gcc_modet:public goto_cc_modet
     bool _produce_hybrid_binary);
 
 protected:
+  gcc_message_handlert gcc_message_handler;
+
   const bool produce_hybrid_binary;
 
   const bool act_as_ld;
   std::string native_tool_name;
-
+  
   int preprocess(
     const std::string &language,
     const std::string &src,
diff --git a/src/goto-cc/goto_cc_mode.cpp b/src/goto-cc/goto_cc_mode.cpp
index a58597e7b9b..225a703e838 100644
--- a/src/goto-cc/goto_cc_mode.cpp
+++ b/src/goto-cc/goto_cc_mode.cpp
@@ -35,11 +35,11 @@ Function: goto_cc_modet::goto_cc_modet
 
 goto_cc_modet::goto_cc_modet(
   goto_cc_cmdlinet &_cmdline,
-  const std::string &_base_name):
-  language_uit(_cmdline, ui_message_handler),
-  ui_message_handler(_cmdline, "goto-cc " CBMC_VERSION),
-  base_name(_base_name),
-  cmdline(_cmdline)
+  const std::string &_base_name,
+  message_handlert &_message_handler):
+  messaget(_message_handler),
+  cmdline(_cmdline),
+  base_name(_base_name)
 {
   register_languages();
 }
diff --git a/src/goto-cc/goto_cc_mode.h b/src/goto-cc/goto_cc_mode.h
index 848e7e4370f..d25fbb750b5 100644
--- a/src/goto-cc/goto_cc_mode.h
+++ b/src/goto-cc/goto_cc_mode.h
@@ -15,7 +15,7 @@ Date: June 2006
 
 #include "goto_cc_cmdline.h"
 
-class goto_cc_modet:public language_uit
+class goto_cc_modet:public messaget
 {
 public:
   virtual int main(int argc, const char **argv);
@@ -25,15 +25,15 @@ class goto_cc_modet:public language_uit
   virtual void usage_error();
 
   goto_cc_modet(
-    goto_cc_cmdlinet &_cmdline,
-    const std::string &_base_name);
+    goto_cc_cmdlinet &,
+    const std::string &_base_name,
+    message_handlert &);
   ~goto_cc_modet();
 
 protected:
-  ui_message_handlert ui_message_handler;
+  goto_cc_cmdlinet &cmdline;
   const std::string base_name;
   void register_languages();
-  goto_cc_cmdlinet &cmdline;
 };
 
 #endif // CPROVER_GOTO_CC_GOTO_CC_MODE_H
diff --git a/src/goto-cc/ld_mode.cpp b/src/goto-cc/ld_mode.cpp
new file mode 100644
index 00000000000..134c7aa4f26
--- /dev/null
+++ b/src/goto-cc/ld_mode.cpp
@@ -0,0 +1,331 @@
+/*******************************************************************\
+
+Module: LD Mode
+
+Author: Daniel Kroening, 2013
+
+\*******************************************************************/
+
+#ifdef _WIN32
+#define EX_OK 0
+#define EX_USAGE 64
+#define EX_SOFTWARE 70
+#else
+#include <sysexits.h>
+#endif
+
+#include <iostream>
+
+#include <util/string2int.h>
+#include <util/config.h>
+
+#include <cbmc/version.h>
+
+#include "compile.h"
+#include "ld_mode.h"
+
+/*******************************************************************\
+
+Function: ld_modet::doit
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: does it.
+
+\*******************************************************************/
+
+int ld_modet::doit()
+{
+  if(cmdline.isset("help"))
+  {
+    help();
+    return EX_OK;
+  }
+
+  unsigned int verbosity=1;
+
+  compilet compiler(cmdline);
+
+  if(cmdline.isset('v') || cmdline.isset('V'))
+  {
+    // This a) prints the version and b) increases verbosity.
+    // Linking continues, don't exit!
+
+    std::cout << "GNU ld version 2.16.91 20050610 (goto-cc " CBMC_VERSION ")\n";
+
+    // 'V' should also print some supported "emulations".
+  }
+
+  if(cmdline.isset("version"))
+  {
+    std::cout << "GNU ld version 2.16.91 20050610 (goto-cc " CBMC_VERSION ")\n";
+    std::cout << "Copyright (C) 2006-2014 Daniel Kroening, Christoph Wintersteiger\n";
+    return EX_OK; // Exit!
+  }
+
+  if(cmdline.isset("verbosity"))
+    verbosity=unsafe_string2int(cmdline.get_value("verbosity"));
+
+  compiler.set_message_handler(get_message_handler());
+  message_handler.set_verbosity(verbosity);
+
+  if(produce_hybrid_binary)
+    debug() << "LD mode (hybrid)" << eom;
+  else
+    debug() << "LD mode" << eom;
+
+  // get configuration
+  config.set(cmdline);
+
+  // determine actions to be undertaken
+  compiler.mode=compilet::LINK_LIBRARY;
+
+  compiler.object_file_extension="o";
+
+  if(cmdline.isset('L'))
+    compiler.library_paths=cmdline.get_values('L');
+    // Don't add the system paths!
+
+  if(cmdline.isset("library-path"))
+    compiler.library_paths=cmdline.get_values("library-path");
+    // Don't add the system paths!
+
+  if(cmdline.isset('l'))
+    compiler.libraries=cmdline.get_values('l');
+
+  if(cmdline.isset("library"))
+    compiler.libraries=cmdline.get_values("library");
+
+  if(cmdline.isset('o'))
+  {
+    // given gcc -o file1 -o file2,
+    // gcc will output to file2, not file1
+    compiler.output_file_object=cmdline.get_values('o').back();
+    compiler.output_file_executable=cmdline.get_values('o').back();
+  }
+  else if(cmdline.isset("output"))
+  {
+    // given gcc -o file1 -o file2,
+    // gcc will output to file2, not file1
+    compiler.output_file_object=cmdline.get_values("output").back();
+    compiler.output_file_executable=cmdline.get_values("output").back();
+  }
+  else
+  {
+    // defaults
+    compiler.output_file_object="";
+    compiler.output_file_executable="a.out";
+  }
+
+  // do all the rest
+  if(compiler.doit())
+    return 1; // ld uses exit code 1 for all sorts of errors
+
+  #if 0
+  if(produce_hybrid_binary)
+  {
+    if(gcc_hybrid_binary(original_args))
+      result=true;
+  }
+  #endif
+
+  return EX_OK;
+}
+
+/*******************************************************************\
+
+Function: ld_modet::gcc_hybrid_binary
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+#if 0
+int ld_modet::gcc_hybrid_binary(const cmdlinet::argst &input_files)
+{
+  if(input_files.empty())
+    return 0;
+
+  std::list<std::string> output_files;
+
+  if(cmdline.isset('c'))
+  {
+    if(cmdline.isset('o'))
+    {
+      // there should be only one input file
+      output_files.push_back(cmdline.get_value('o'));
+    }
+    else
+    {
+      for(cmdlinet::argst::const_iterator
+          i_it=input_files.begin();
+          i_it!=input_files.end();
+          i_it++)
+      {
+        if(is_supported_source_file(*i_it) && cmdline.isset('c'))
+          output_files.push_back(get_base_name(*i_it)+".o");
+      }
+    }
+  }
+  else
+  {
+    // -c is not given
+    if(cmdline.isset('o'))
+      output_files.push_back(cmdline.get_value('o'));
+    else
+      output_files.push_back("a.out");
+  }
+
+  if(output_files.empty()) return 0;
+
+  debug("Running gcc to generate hybrid binary");
+
+  // save the goto-cc output files
+  for(std::list<std::string>::const_iterator
+      it=output_files.begin();
+      it!=output_files.end();
+      it++)
+  {
+    rename(it->c_str(), (*it+".goto-cc-saved").c_str());
+  }
+
+  // build new argv
+  std::vector<std::string> new_argv;
+
+  new_argv.reserve(cmdline.parsed_argv.size());
+
+  bool skip_next=false;
+
+  for(ld_cmdlinet::parsed_argvt::const_iterator
+      it=cmdline.parsed_argv.begin();
+      it!=cmdline.parsed_argv.end();
+      it++)
+  {
+    if(skip_next)
+    {
+      // skip
+      skip_next=false;
+    }
+    else if(it->arg=="--verbosity")
+    {
+      // ignore here
+      skip_next=true;
+    }
+    else
+      new_argv.push_back(it->arg);
+  }
+
+  // overwrite argv[0]
+  assert(new_argv.size()>=1);
+  new_argv[0]="gcc";
+
+  #if 0
+  std::cout << "RUN:";
+  for(std::size_t i=0; i<new_argv.size(); i++)
+    std::cout << " " << new_argv[i];
+  std::cout << std::endl;
+  #endif
+
+  int result=run("gcc", new_argv);
+
+  // merge output from gcc with goto-binaries
+  // using objcopy
+  for(std::list<std::string>::const_iterator
+      it=output_files.begin();
+      it!=output_files.end();
+      it++)
+  {
+    #ifdef __linux__
+    debug("merging "+*it);
+
+    if(!cmdline.isset('c'))
+    {
+      // remove any existing goto-cc section
+      std::vector<std::string> objcopy_argv;
+
+      objcopy_argv.push_back("objcopy");
+      objcopy_argv.push_back("--remove-section=goto-cc");
+      objcopy_argv.push_back(*it);
+
+      run(objcopy_argv[0], objcopy_argv);
+    }
+
+    // now add goto-binary as goto-cc section
+    std::string saved=*it+".goto-cc-saved";
+
+    std::vector<std::string> objcopy_argv;
+
+    objcopy_argv.push_back("objcopy");
+    objcopy_argv.push_back("--add-section");
+    objcopy_argv.push_back("goto-cc="+saved);
+    objcopy_argv.push_back(*it);
+
+    run(objcopy_argv[0], objcopy_argv);
+
+    remove(saved.c_str());
+
+    #elif defined(__APPLE__)
+    // Mac
+
+    for(std::list<std::string>::const_iterator
+        it=output_files.begin();
+        it!=output_files.end();
+        it++)
+    {
+      debug("merging "+*it);
+
+      std::vector<std::string> lipo_argv;
+
+      // now add goto-binary as hppa7100LC section
+      std::string saved=*it+".goto-cc-saved";
+
+      lipo_argv.push_back("lipo");
+      lipo_argv.push_back(*it);
+      lipo_argv.push_back("-create");
+      lipo_argv.push_back("-arch");
+      lipo_argv.push_back("hppa7100LC");
+      lipo_argv.push_back(saved);
+      lipo_argv.push_back("-output");
+      lipo_argv.push_back(*it);
+
+      run(lipo_argv[0], lipo_argv);
+
+      remove(saved.c_str());
+    }
+
+    return 0;
+
+    #else
+
+    error() << "binary merging not implemented for this architecture" << eom;
+    return 1;
+
+    #endif
+  }
+
+  return result!=0;
+}
+#endif
+
+/*******************************************************************\
+
+Function: ld_modet::help_mode
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: display command line help
+
+\*******************************************************************/
+
+void ld_modet::help_mode()
+{
+  std::cout << "goto-ld understands the options of ld plus the following.\n\n";
+}
diff --git a/src/goto-cc/ld_mode.h b/src/goto-cc/ld_mode.h
new file mode 100644
index 00000000000..1fb112432aa
--- /dev/null
+++ b/src/goto-cc/ld_mode.h
@@ -0,0 +1,42 @@
+/*******************************************************************\
+
+Module: Base class for command line interpretation
+
+Author: CM Wintersteiger
+
+Date: June 2006
+
+\*******************************************************************/
+
+#ifndef CPROVER_GOTO_CC_LD_MODE_H
+#define CPROVER_GOTO_CC_LD_MODE_H
+
+#include <util/cout_message.h>
+
+#include "goto_cc_mode.h"
+#include "ld_cmdline.h"
+
+class ld_modet:public goto_cc_modet
+{
+public:
+  int doit() final;
+  void help_mode() final;
+
+  explicit ld_modet(ld_cmdlinet &_ld_cmdline):
+    goto_cc_modet(_ld_cmdline, message_handler),
+    produce_hybrid_binary(false),
+    cmdline(_ld_cmdline)
+  {
+  }
+
+  bool produce_hybrid_binary;
+
+protected:
+  ld_cmdlinet &cmdline;
+  gcc_message_handlert message_handler;
+
+  //int gcc_hybrid_binary(const cmdlinet::argst &input_files);
+  //static bool is_supported_source_file(const std::string &);
+};
+
+#endif // CPROVER_GOTO_CC_LD_MODE_H
diff --git a/src/goto-cc/ms_cl_mode.cpp b/src/goto-cc/ms_cl_mode.cpp
index 73a06455467..86aaf3f0a3d 100644
--- a/src/goto-cc/ms_cl_mode.cpp
+++ b/src/goto-cc/ms_cl_mode.cpp
@@ -69,8 +69,8 @@ int ms_cl_modet::doit()
   if(cmdline.isset("verbosity"))
     verbosity=unsafe_string2unsigned(cmdline.get_value("verbosity"));
 
-  compiler.ui_message_handler.set_verbosity(verbosity);
-  ui_message_handler.set_verbosity(verbosity);
+  compiler.set_message_handler(get_message_handler());
+  message_handler.set_verbosity(verbosity);
 
   debug() << "Visual Studio mode" << eom;
 
diff --git a/src/goto-cc/ms_cl_mode.h b/src/goto-cc/ms_cl_mode.h
index e1ae2726c64..673c6efed35 100644
--- a/src/goto-cc/ms_cl_mode.h
+++ b/src/goto-cc/ms_cl_mode.h
@@ -11,6 +11,8 @@ 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 "goto_cc_mode.h"
 #include "ms_cl_cmdline.h"
 
@@ -23,13 +25,14 @@ class ms_cl_modet:public goto_cc_modet
   ms_cl_modet(
     ms_cl_cmdlinet &_ms_cl_cmdline,
     const std::string &_base_name):
-    goto_cc_modet(_ms_cl_cmdline, _base_name),
+    goto_cc_modet(_ms_cl_cmdline, _base_name, message_handler),
     cmdline(_ms_cl_cmdline)
   {
   }
 
 protected:
   ms_cl_cmdlinet &cmdline;
+  console_message_handlert message_handler;
 };
 
 #endif // CPROVER_GOTO_CC_MS_CL_MODE_H
diff --git a/src/util/cout_message.cpp b/src/util/cout_message.cpp
index 6b63f8625ad..d4936d5ad53 100644
--- a/src/util/cout_message.cpp
+++ b/src/util/cout_message.cpp
@@ -135,3 +135,68 @@ void console_message_handlert::print(
     std::cerr << message << '\n' << std::flush;
   #endif
 }
+
+/*******************************************************************\
+
+Function: gcc_message_handlert::print
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void gcc_message_handlert::print(
+  unsigned level,
+  const std::string &message,
+  int sequence_number,
+  const source_locationt &location)
+{
+  std::string dest;
+
+  const irep_idt &file=location.get_file();
+  const irep_idt &line=location.get_line();
+  const irep_idt &function=location.get_function();
+  
+  if(!function.empty())
+  {
+    if(!file.empty())
+      dest+=id2string(file)+":";
+    if(dest!="") dest+=' ';
+    dest+="In function '"+id2string(function)+"':\n";
+  }
+
+  if(!line.empty())
+  {
+    if(!file.empty())
+      dest+=id2string(file)+":";
+
+    dest+=id2string(line)+":"+id2string(line)+":";
+  }
+
+  dest+=message;
+
+  print(level, dest);
+}
+
+/*******************************************************************\
+
+Function: gcc_message_handlert::print
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void gcc_message_handlert::print(
+  unsigned level,
+  const std::string &message)
+{
+  // gcc appears to send everything to cerr
+  std::cerr << message << '\n' << std::flush;
+}
diff --git a/src/util/cout_message.h b/src/util/cout_message.h
index 0cedb2b790c..ab78148c6d6 100644
--- a/src/util/cout_message.h
+++ b/src/util/cout_message.h
@@ -15,21 +15,42 @@ class cout_message_handlert:public message_handlert
 {
 public:
   // all messages go to cout
-  virtual void print(unsigned level, const std::string &message);
+  virtual void print(
+    unsigned level,
+    const std::string &message) override;
 };
 
 class cerr_message_handlert:public message_handlert
 {
 public:
   // all messages go to cerr
-  virtual void print(unsigned level, const std::string &message);
+  virtual void print(
+    unsigned level,
+    const std::string &message) override;
 };
 
 class console_message_handlert:public message_handlert
 {
 public:
   // level 4 and upwards go to cout, level 1-3 to cerr
-  virtual void print(unsigned level, const std::string &message);
+  virtual void print(
+    unsigned level,
+    const std::string &message) override;
+};
+
+class gcc_message_handlert:public message_handlert
+{
+public:
+  // aims to imitate the messages gcc prints
+  virtual void print(
+    unsigned level,
+    const std::string &message) override;
+
+  virtual void print(
+    unsigned level,
+    const std::string &message,
+    int sequence_number,
+    const source_locationt &location) override;
 };
 
 #endif // CPROVER_UTIL_COUT_MESSAGE_H