Merge pull request #517 from diffblue/gcc-errors2

kroening · web-flow · commit 12c051b323ff · 2017-02-09T21:38:45.000Z
gcc-style error messages
diff --git a/regression/ansi-c/function_return1/test.desc b/regression/ansi-c/function_return1/test.desc
@@ -1,7 +1,7 @@
 CORE
 main.c
 --verbosity 2
-^file main.c line 3 function fun: function has return void but a return statement returning signed int$
+^main.c:3:1: warning: function has return void but a return statement returning signed int$
 ^SIGNAL=0$
 
 --
diff --git a/regression/ansi-c/struct6/test.desc b/regression/ansi-c/struct6/test.desc
@@ -3,6 +3,6 @@ main.c
 
 ^EXIT=\(64\|1\)$
 ^SIGNAL=0$
-^file main.c line 2: incomplete type not permitted here$
+^main.c:2:1: error: incomplete type not permitted here$
 ^CONVERSION ERROR$
 --
diff --git a/regression/ansi-c/struct7/test.desc b/regression/ansi-c/struct7/test.desc
@@ -3,6 +3,6 @@ main.c
 
 ^EXIT=\(64\|1\)$
 ^SIGNAL=0$
-^file main.c line 4: duplicate member x$
+^main.c:4:1: error: duplicate member .*$
 ^CONVERSION ERROR$
 --
diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp
@@ -918,7 +918,7 @@ void c_typecheck_baset::typecheck_compound_body(
       if(!members.insert(it->get_name()).second)
       {
         error().source_location=it->source_location();
-        error() << "duplicate member " << it->get_name() << eom;
+        error() << "duplicate member '" << it->get_name() << '\'' << eom;
         throw 0;
       }
     }
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -11,20 +11,24 @@ 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,
     const std::string &_base_name,
     bool _produce_hybrid_binary);
 
 protected:
+  gcc_message_handlert gcc_message_handler;
+
   const bool produce_hybrid_binary;
 
   const bool act_as_ld;
diff --git 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
@@ -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/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
@@ -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
@@ -135,3 +135,79 @@ 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)
+{
+  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();
+  
+  std::string dest;
+
+  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)+":";
+
+    if(column.empty())
+      dest+="1: ";
+    else
+      dest+=id2string(column)+": ";
+
+    if(level==message_clientt::M_ERROR)
+      dest+="error: ";
+    else if(level==message_clientt::M_WARNING)
+      dest+="warning: ";
+  }
+
+  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

Original file line number	Diff line number	Diff line change
`@@ -918,7 +918,7 @@ void c_typecheck_baset::typecheck_compound_body(`
`918`	`918`	`if(!members.insert(it->get_name()).second)`
`919`	`919`	`{`
`920`	`920`	`error().source_location=it->source_location();`
`921`		`- error() << "duplicate member " << it->get_name() << eom;`
	`921`	`+ error() << "duplicate member '" << it->get_name() << '\'' << eom;`
`922`	`922`	`throw 0;`
`923`	`923`	`}`
`924`	`924`	`}`