diff --git a/regression/ansi-c/function_return1/test.desc b/regression/ansi-c/function_return1/test.desc index 59f820626c6..78396740555 100644 --- 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 index 533aff79467..d97230c659f 100644 --- 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 index b9bd5b62b50..9c24052d9c5 100644 --- 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 index 78a41a662b5..dfe897a4b1f 100644 --- 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 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 + #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 #include #include +#include #include @@ -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 + #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 + #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..b37b87448d6 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 + #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,6 +27,8 @@ 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; 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/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 + #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..6ed5125ba47 100644 --- 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 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