From d209b90c58f546199fa265774f45cdc5a05f1127 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 7 Jul 2016 13:49:55 +0200 Subject: [PATCH 1/7] cout/cerr message handlers are stream_message_handlert --- src/util/cout_message.cpp | 24 ++++++------------------ src/util/cout_message.h | 16 ++++++---------- src/util/message.h | 7 ++++++- 3 files changed, 18 insertions(+), 29 deletions(-) diff --git a/src/util/cout_message.cpp b/src/util/cout_message.cpp index 393ec62432f..2080e686b7c 100644 --- a/src/util/cout_message.cpp +++ b/src/util/cout_message.cpp @@ -20,7 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com /*******************************************************************\ -Function: cout_message_handlert::print +Function: cout_message_handlert::cout_message_handlert Inputs: @@ -30,23 +30,14 @@ Function: cout_message_handlert::print \*******************************************************************/ -void cout_message_handlert::print( - unsigned level, - const std::string &message) +cout_message_handlert::cout_message_handlert(): + stream_message_handlert(std::cout) { - if(verbosity>=level) - { - std::cout << message << '\n'; - - // We flush for level 6 or below. - if(level<=6) - std::cout << std::flush; - } } /*******************************************************************\ -Function: cerr_message_handlert::print +Function: cerr_message_handlert::cerr_message_handlert Inputs: @@ -56,12 +47,9 @@ Function: cerr_message_handlert::print \*******************************************************************/ -void cerr_message_handlert::print( - unsigned level, - const std::string &message) +cerr_message_handlert::cerr_message_handlert(): + stream_message_handlert(std::cerr) { - if(verbosity>=level) - std::cerr << message << '\n' << std::flush; } /*******************************************************************\ diff --git a/src/util/cout_message.h b/src/util/cout_message.h index ab78148c6d6..108dba8d5d2 100644 --- a/src/util/cout_message.h +++ b/src/util/cout_message.h @@ -11,22 +11,18 @@ Author: Daniel Kroening, kroening@kroening.com #include "message.h" -class cout_message_handlert:public message_handlert +class cout_message_handlert:public stream_message_handlert { public: - // all messages go to cout - virtual void print( - unsigned level, - const std::string &message) override; + // all messages go to stdout + cout_message_handlert(); }; -class cerr_message_handlert:public message_handlert +class cerr_message_handlert:public stream_message_handlert { public: - // all messages go to cerr - virtual void print( - unsigned level, - const std::string &message) override; + // all messages go to stderr + cerr_message_handlert(); }; class console_message_handlert:public message_handlert diff --git a/src/util/message.h b/src/util/message.h index b92fb8f3dfd..db0c9e8c90d 100644 --- a/src/util/message.h +++ b/src/util/message.h @@ -65,7 +65,12 @@ class stream_message_handlert:public message_handlert } virtual void print(unsigned level, const std::string &message) - { out << message << '\n'; } + { + if(verbosity>=level) + { + out << message << '\n'; + } + } protected: std::ostream &out; From e3e74b0df2096395374441281445334bd12a97b6 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 7 Jul 2016 09:31:27 +0200 Subject: [PATCH 2/7] Message handlers maintain counters of messages per level Works at all message levels, instead of the previous get_errors_found workarounds. --- src/ansi-c/ansi_c_typecheck.cpp | 5 ++++- src/cpp/cpp_typecheck.cpp | 5 ++++- src/goto-programs/goto_convert.cpp | 9 ++++++--- src/goto-programs/goto_convert_functions.cpp | 18 +++++++++++------ src/jsil/jsil_typecheck.cpp | 5 ++++- src/util/cout_message.cpp | 2 ++ src/util/message.cpp | 21 ++++++++++++++++++++ src/util/message.h | 14 ++++++++++++- src/util/ui_message.cpp | 4 ++++ 9 files changed, 70 insertions(+), 13 deletions(-) diff --git a/src/ansi-c/ansi_c_typecheck.cpp b/src/ansi-c/ansi_c_typecheck.cpp index 08da6bbae01..79efef1b183 100644 --- a/src/ansi-c/ansi_c_typecheck.cpp +++ b/src/ansi-c/ansi_c_typecheck.cpp @@ -72,6 +72,9 @@ bool ansi_c_typecheck( message_handlert &message_handler, const namespacet &ns) { + const unsigned errors_before= + message_handler.get_message_count(messaget::M_ERROR); + symbol_tablet symbol_table; ansi_c_parse_treet ansi_c_parse_tree; @@ -99,5 +102,5 @@ bool ansi_c_typecheck( ansi_c_typecheck.error() << e << messaget::eom; } - return ansi_c_typecheck.get_error_found(); + return message_handler.get_message_count(messaget::M_ERROR)!=errors_before; } diff --git a/src/cpp/cpp_typecheck.cpp b/src/cpp/cpp_typecheck.cpp index fe8a9f063d7..f9c2e8fd4b3 100644 --- a/src/cpp/cpp_typecheck.cpp +++ b/src/cpp/cpp_typecheck.cpp @@ -178,6 +178,9 @@ bool cpp_typecheck( message_handlert &message_handler, const namespacet &ns) { + const unsigned errors_before= + message_handler.get_message_count(messaget::M_ERROR); + symbol_tablet symbol_table; cpp_parse_treet cpp_parse_tree; @@ -204,7 +207,7 @@ bool cpp_typecheck( cpp_typecheck.error() << e << messaget::eom; } - return cpp_typecheck.get_error_found(); + return message_handler.get_message_count(messaget::M_ERROR)!=errors_before; } /*******************************************************************\ diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index 25118d0b223..031ba5f142a 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -2866,6 +2866,9 @@ void goto_convert( goto_programt &dest, message_handlert &message_handler) { + const unsigned errors_before= + message_handler.get_message_count(messaget::M_ERROR); + goto_convertt goto_convert(symbol_table, message_handler); try @@ -2876,20 +2879,20 @@ void goto_convert( catch(int) { goto_convert.error(); - throw 0; } catch(const char *e) { goto_convert.error() << e << messaget::eom; - throw 0; } catch(const std::string &e) { goto_convert.error() << e << messaget::eom; - throw 0; } + + if(message_handler.get_message_count(messaget::M_ERROR)!=errors_before) + throw 0; } /*******************************************************************\ diff --git a/src/goto-programs/goto_convert_functions.cpp b/src/goto-programs/goto_convert_functions.cpp index b25d8870f09..c287338b9c9 100644 --- a/src/goto-programs/goto_convert_functions.cpp +++ b/src/goto-programs/goto_convert_functions.cpp @@ -330,6 +330,9 @@ void goto_convert( goto_functionst &functions, message_handlert &message_handler) { + const unsigned errors_before= + message_handler.get_message_count(messaget::M_ERROR); + goto_convert_functionst goto_convert_functions( symbol_table, functions, message_handler); @@ -341,20 +344,20 @@ void goto_convert( catch(int) { goto_convert_functions.error(); - throw 0; } catch(const char *e) { goto_convert_functions.error() << e << messaget::eom; - throw 0; } catch(const std::string &e) { goto_convert_functions.error() << e << messaget::eom; - throw 0; } + + if(message_handler.get_message_count(messaget::M_ERROR)!=errors_before) + throw 0; } /*******************************************************************\ @@ -375,6 +378,9 @@ void goto_convert( goto_functionst &functions, message_handlert &message_handler) { + const unsigned errors_before= + message_handler.get_message_count(messaget::M_ERROR); + goto_convert_functionst goto_convert_functions( symbol_table, functions, message_handler); @@ -386,18 +392,18 @@ void goto_convert( catch(int) { goto_convert_functions.error(); - throw 0; } catch(const char *e) { goto_convert_functions.error() << e << messaget::eom; - throw 0; } catch(const std::string &e) { goto_convert_functions.error() << e << messaget::eom; - throw 0; } + + if(message_handler.get_message_count(messaget::M_ERROR)!=errors_before) + throw 0; } diff --git a/src/jsil/jsil_typecheck.cpp b/src/jsil/jsil_typecheck.cpp index a644f1acf99..0e8168b7fbf 100644 --- a/src/jsil/jsil_typecheck.cpp +++ b/src/jsil/jsil_typecheck.cpp @@ -1398,6 +1398,9 @@ bool jsil_typecheck( message_handlert &message_handler, const namespacet &ns) { + const unsigned errors_before= + message_handler.get_message_count(messaget::M_ERROR); + symbol_tablet symbol_table; jsil_typecheckt jsil_typecheck( @@ -1424,5 +1427,5 @@ bool jsil_typecheck( jsil_typecheck.error() << e << messaget::eom; } - return jsil_typecheck.get_error_found(); + return message_handler.get_message_count(messaget::M_ERROR)!=errors_before; } diff --git a/src/util/cout_message.cpp b/src/util/cout_message.cpp index 2080e686b7c..42153e9e422 100644 --- a/src/util/cout_message.cpp +++ b/src/util/cout_message.cpp @@ -71,6 +71,8 @@ void console_message_handlert::print( if(verbosity1)?STD_OUTPUT_HANDLE:STD_ERROR_HANDLE); diff --git a/src/util/message.cpp b/src/util/message.cpp index 21a67433609..0fe90c1239b 100644 --- a/src/util/message.cpp +++ b/src/util/message.cpp @@ -67,6 +67,27 @@ void message_handlert::print( /*******************************************************************\ +Function: message_handlert::print + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void message_handlert::print( + unsigned level, + const std::string &message) +{ + if(level>=message_count.size()) + message_count.resize(level+1, 0); + ++message_count[level]; +} + +/*******************************************************************\ + Function: messaget::print Inputs: diff --git a/src/util/message.h b/src/util/message.h index db0c9e8c90d..6576c705907 100644 --- a/src/util/message.h +++ b/src/util/message.h @@ -18,7 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com class message_handlert { public: - message_handlert():verbosity(10) + message_handlert():verbosity(10), message_count(10, 0) { } @@ -37,8 +37,17 @@ class message_handlert void set_verbosity(unsigned _verbosity) { verbosity=_verbosity; } unsigned get_verbosity() const { return verbosity; } + inline unsigned get_message_count(unsigned level) const + { + if(level>=message_count.size()) + return 0; + + return message_count[level]; + } + protected: unsigned verbosity; + std::vector message_count; }; class null_message_handlert:public message_handlert @@ -46,6 +55,7 @@ class null_message_handlert:public message_handlert public: virtual void print(unsigned level, const std::string &message) { + message_handlert::print(level, message); } virtual void print( @@ -54,6 +64,7 @@ class null_message_handlert:public message_handlert int sequence_number, const source_locationt &location) { + print(level, message); } }; @@ -68,6 +79,7 @@ class stream_message_handlert:public message_handlert { if(verbosity>=level) { + message_handlert::print(level, message); out << message << '\n'; } } diff --git a/src/util/ui_message.cpp b/src/util/ui_message.cpp index 1cc32ecf356..adbce5a676f 100644 --- a/src/util/ui_message.cpp +++ b/src/util/ui_message.cpp @@ -156,6 +156,8 @@ void ui_message_handlert::print( { case uit::PLAIN: { + message_handlert::print(level, message); + console_message_handlert console_message_handler; console_message_handler.print(level, message); } @@ -203,6 +205,8 @@ void ui_message_handlert::print( case uit::XML_UI: case uit::JSON_UI: { + message_handlert::print(level, message); + std::string tmp_message(message); if(!tmp_message.empty() && *tmp_message.rbegin()=='\n') From aa8c5e97f91f7e8a9530bb5dd442421427944c35 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 7 Jul 2016 11:28:25 +0200 Subject: [PATCH 3/7] Support flush at eom to ensure complete output --- src/util/cout_message.cpp | 35 ++++++++++++++++++++++++++--------- src/util/cout_message.h | 2 ++ src/util/message.h | 20 +++++++++++++++++++- src/util/ui_message.cpp | 32 ++++++++++++++++++++++++++++++++ src/util/ui_message.h | 2 ++ 5 files changed, 81 insertions(+), 10 deletions(-) diff --git a/src/util/cout_message.cpp b/src/util/cout_message.cpp index 42153e9e422..c7a5f09565c 100644 --- a/src/util/cout_message.cpp +++ b/src/util/cout_message.cpp @@ -101,30 +101,47 @@ void console_message_handlert::print( if(level>=4) { std::cout << message << '\n'; - - if(level<=6) - std::cout << std::flush; } else - std::cerr << message << '\n' << std::flush; + std::cerr << message << '\n'; } #else - // We flush after messages of level 6 or lower. - // We don't for messages of level 7 or higher to improve performance, - // in particular when writing to NFS. // Messages level 3 or lower go to cerr, messages level 4 or // above go to cout. if(level>=4) { std::cout << message << '\n'; + } + else + std::cerr << message << '\n'; + #endif +} + +/*******************************************************************\ + +Function: console_message_handlert::flush + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void console_message_handlert::flush(unsigned level) +{ + // We flush after messages of level 6 or lower. + // We don't for messages of level 7 or higher to improve performance, + // in particular when writing to NFS. + if(level>=4) + { if(level<=6) std::cout << std::flush; } else - std::cerr << message << '\n' << std::flush; - #endif + std::cerr << std::flush; } /*******************************************************************\ diff --git a/src/util/cout_message.h b/src/util/cout_message.h index 108dba8d5d2..71f9ce83f4f 100644 --- a/src/util/cout_message.h +++ b/src/util/cout_message.h @@ -32,6 +32,8 @@ class console_message_handlert:public message_handlert virtual void print( unsigned level, const std::string &message) override; + + virtual void flush(unsigned level) override; }; class gcc_message_handlert:public message_handlert diff --git a/src/util/message.h b/src/util/message.h index 6576c705907..dd7b97a270d 100644 --- a/src/util/message.h +++ b/src/util/message.h @@ -30,6 +30,11 @@ class message_handlert int sequence_number, const source_locationt &location); + virtual void flush(unsigned level) + { + // no-op by default + } + virtual ~message_handlert() { } @@ -84,6 +89,11 @@ class stream_message_handlert:public message_handlert } } + virtual void flush(unsigned level) + { + out << std::flush; + } + protected: std::ostream &out; }; @@ -216,7 +226,15 @@ class messaget:public message_clientt // the printing of the message static inline mstreamt &eom(mstreamt &m) { - m.message.print(m.message_level, m.str(), -1, m.source_location); + if(m.message.message_handler) + { + m.message.message_handler->print( + m.message_level, + m.str(), + -1, + m.source_location); + m.message.message_handler->flush(m.message_level); + } m.clear(); // clears error bits m.str(std::string()); // clears the string m.source_location.clear(); diff --git a/src/util/ui_message.cpp b/src/util/ui_message.cpp index adbce5a676f..d1eab2338dc 100644 --- a/src/util/ui_message.cpp +++ b/src/util/ui_message.cpp @@ -323,3 +323,35 @@ void ui_message_handlert::json_ui_msg( // a trailing comma. std::cout << ",\n" << result; } + +/*******************************************************************\ + +Function: ui_message_handlert::flush + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void ui_message_handlert::flush(unsigned level) +{ + switch(get_ui()) + { + case uit::PLAIN: + { + console_message_handlert console_message_handler; + console_message_handler.flush(level); + } + break; + + case uit::XML_UI: + case uit::JSON_UI: + { + std::cout << std::flush; + } + break; + } +} diff --git a/src/util/ui_message.h b/src/util/ui_message.h index 59cc5c21009..c4e70e6b4cd 100644 --- a/src/util/ui_message.h +++ b/src/util/ui_message.h @@ -31,6 +31,8 @@ class ui_message_handlert:public message_handlert _ui=__ui; } + virtual void flush(unsigned level); + protected: uit _ui; From 70755fcbcc9d0ff2cbd43380dcb89dd868afef1b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 7 Jul 2016 11:34:56 +0200 Subject: [PATCH 4/7] Removed legacy_typecheckt interface, use new message counters --- src/util/cout_message.cpp | 6 ++++-- src/util/message.h | 5 ++--- src/util/typecheck.cpp | 9 +++++++-- src/util/typecheck.h | 17 +++++++---------- src/util/ui_message.cpp | 6 ++---- 5 files changed, 22 insertions(+), 21 deletions(-) diff --git a/src/util/cout_message.cpp b/src/util/cout_message.cpp index c7a5f09565c..a25be15e656 100644 --- a/src/util/cout_message.cpp +++ b/src/util/cout_message.cpp @@ -68,11 +68,11 @@ void console_message_handlert::print( unsigned level, const std::string &message) { + message_handlert::print(level, message); + if(verbosity1)?STD_OUTPUT_HANDLE:STD_ERROR_HANDLE); @@ -217,6 +217,8 @@ void gcc_message_handlert::print( unsigned level, const std::string &message) { + message_handlert::print(level, message); + // gcc appears to send everything to cerr if(verbosity>=level) std::cerr << message << '\n' << std::flush; diff --git a/src/util/message.h b/src/util/message.h index dd7b97a270d..5e902409e5a 100644 --- a/src/util/message.h +++ b/src/util/message.h @@ -82,11 +82,10 @@ class stream_message_handlert:public message_handlert virtual void print(unsigned level, const std::string &message) { + message_handlert::print(level, message); + if(verbosity>=level) - { - message_handlert::print(level, message); out << message << '\n'; - } } virtual void flush(unsigned level) diff --git a/src/util/typecheck.cpp b/src/util/typecheck.cpp index 67b695e53fa..020c202015d 100644 --- a/src/util/typecheck.cpp +++ b/src/util/typecheck.cpp @@ -22,6 +22,11 @@ Author: Daniel Kroening, kroening@kroening.com bool typecheckt::typecheck_main() { + assert(message_handler); + + const unsigned errors_before= + message_handler->get_message_count(messaget::M_ERROR); + try { typecheck(); @@ -29,7 +34,7 @@ bool typecheckt::typecheck_main() catch(int) { - error_found=true; + error(); } catch(const char *e) @@ -42,5 +47,5 @@ bool typecheckt::typecheck_main() error() << e << eom; } - return error_found; + return message_handler->get_message_count(messaget::M_ERROR)!=errors_before; } diff --git a/src/util/typecheck.h b/src/util/typecheck.h index ee80f6e42f0..1d5cd51decc 100644 --- a/src/util/typecheck.h +++ b/src/util/typecheck.h @@ -16,30 +16,27 @@ class typecheckt:public messaget { public: explicit typecheckt(message_handlert &_message_handler): - messaget(_message_handler), - error_found(false) + messaget(_message_handler) { } virtual ~typecheckt() { } - mstreamt &error() + // not pretty, but makes transition easier + void err_location(const source_locationt &loc) { - error_found=true; - return messaget::error(); + messaget::error().source_location=loc; } // not pretty, but makes transition easier void err_location(const exprt &src) { - error().source_location=src.find_source_location(); + err_location(src.find_source_location()); } - bool error_found; - - bool get_error_found() const + void err_location(const typet &src) { - return error_found; + err_location(src.source_location()); } protected: diff --git a/src/util/ui_message.cpp b/src/util/ui_message.cpp index d1eab2338dc..43f284fb444 100644 --- a/src/util/ui_message.cpp +++ b/src/util/ui_message.cpp @@ -156,8 +156,6 @@ void ui_message_handlert::print( { case uit::PLAIN: { - message_handlert::print(level, message); - console_message_handlert console_message_handler; console_message_handler.print(level, message); } @@ -193,6 +191,8 @@ void ui_message_handlert::print( int sequence_number, const source_locationt &location) { + message_handlert::print(level, message); + if(verbosity>=level) { switch(get_ui()) @@ -205,8 +205,6 @@ void ui_message_handlert::print( case uit::XML_UI: case uit::JSON_UI: { - message_handlert::print(level, message); - std::string tmp_message(message); if(!tmp_message.empty() && *tmp_message.rbegin()=='\n') From 3a55283b37488bd7d7088085723d3d01c3780ed0 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 7 Jul 2016 09:40:19 +0200 Subject: [PATCH 5/7] Removed legacy messaget interface, removed message_clientt --- src/cbmc/cbmc_parse_options.cpp | 2 +- src/clobber/clobber_parse_options.cpp | 2 +- src/goto-cc/compile.cpp | 10 +- src/goto-programs/initialize_goto_model.cpp | 5 +- src/goto-symex/memory_model_pso.cpp | 2 +- src/goto-symex/memory_model_sc.cpp | 2 +- src/goto-symex/memory_model_tso.cpp | 2 +- src/langapi/language_ui.cpp | 5 +- src/solvers/prop/prop_conv.cpp | 8 +- src/solvers/sat/pbs_dimacs_cnf.cpp | 3 +- src/util/cout_message.cpp | 4 +- src/util/message.cpp | 63 +----------- src/util/message.h | 106 ++++++-------------- src/util/parser.cpp | 3 +- 14 files changed, 61 insertions(+), 156 deletions(-) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index f20d666179b..b356658542a 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -655,7 +655,7 @@ int cbmc_parse_optionst::get_goto_program( language->set_message_handler(get_message_handler()); - status("Parsing", filename); + status() << "Parsing " << filename << eom; if(language->parse(infile, filename)) { diff --git a/src/clobber/clobber_parse_options.cpp b/src/clobber/clobber_parse_options.cpp index 7fda29931f0..4c70f7fa22f 100644 --- a/src/clobber/clobber_parse_options.cpp +++ b/src/clobber/clobber_parse_options.cpp @@ -326,7 +326,7 @@ bool clobber_parse_optionst::get_goto_program( language->set_message_handler(get_message_handler()); - status("Parsing", filename); + status() << "Parsing " << filename << eom; if(language->parse(infile, filename)) { diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp index 58f74669c32..fae6623aaf1 100644 --- a/src/goto-cc/compile.cpp +++ b/src/goto-cc/compile.cpp @@ -383,7 +383,7 @@ Function: compilet::link bool compilet::link() { // "compile" hitherto uncompiled functions - print(8, "Compiling functions"); + statistics() << "Compiling functions" << eom; convert_symbols(compiled_functions); // parse object files @@ -554,7 +554,7 @@ bool compilet::parse(const std::string &file_name) if(mode==PREPROCESS_ONLY) { - print(8, "Preprocessing: "+file_name); + statistics() << "Preprocessing: " << file_name << eom; std::ostream *os = &std::cout; std::ofstream ofs; @@ -576,7 +576,7 @@ bool compilet::parse(const std::string &file_name) } else { - print(8, "Parsing: "+file_name); + statistics() << "Parsing: " << file_name << eom; if(language.parse(infile, file_name)) { @@ -608,7 +608,7 @@ bool compilet::parse_stdin() language.set_message_handler(get_message_handler()); - print(8, "Parsing: (stdin)"); + statistics() << "Parsing: (stdin)" << eom; if(mode==PREPROCESS_ONLY) { @@ -872,7 +872,7 @@ void compilet::convert_symbols(goto_functionst &dest) s_it->second.value.id()!="compiled" && s_it->second.value.is_not_nil()) { - print(9, "Compiling "+id2string(s_it->first)); + debug() << "Compiling " << s_it->first << eom; converter.convert_function(s_it->first); s_it->second.value=exprt("compiled"); } diff --git a/src/goto-programs/initialize_goto_model.cpp b/src/goto-programs/initialize_goto_model.cpp index 52a6caeeba2..779593a245b 100644 --- a/src/goto-programs/initialize_goto_model.cpp +++ b/src/goto-programs/initialize_goto_model.cpp @@ -91,7 +91,10 @@ bool initialize_goto_model( if(lf.language==NULL) { - msg.error("failed to figure out type of file", filename); + source_locationt location; + location.set_file(filename); + msg.error().source_location=location; + msg.error() << "failed to figure out type of file" << messaget::eom; return true; } diff --git a/src/goto-symex/memory_model_pso.cpp b/src/goto-symex/memory_model_pso.cpp index 629451fc80b..d21a7f1bb2c 100644 --- a/src/goto-symex/memory_model_pso.cpp +++ b/src/goto-symex/memory_model_pso.cpp @@ -22,7 +22,7 @@ Function: memory_model_psot::operator() void memory_model_psot::operator()(symex_target_equationt &equation) { - print(8, "Adding PSO constraints"); + statistics() << "Adding PSO constraints" << eom; build_event_lists(equation); build_clock_type(equation); diff --git a/src/goto-symex/memory_model_sc.cpp b/src/goto-symex/memory_model_sc.cpp index 7c131269802..59de4870300 100644 --- a/src/goto-symex/memory_model_sc.cpp +++ b/src/goto-symex/memory_model_sc.cpp @@ -24,7 +24,7 @@ Function: memory_model_sct::operator() void memory_model_sct::operator()(symex_target_equationt &equation) { - print(8, "Adding SC constraints"); + statistics() << "Adding SC constraints" << eom; build_event_lists(equation); build_clock_type(equation); diff --git a/src/goto-symex/memory_model_tso.cpp b/src/goto-symex/memory_model_tso.cpp index 1fec15c9bdd..22fd6a1b238 100644 --- a/src/goto-symex/memory_model_tso.cpp +++ b/src/goto-symex/memory_model_tso.cpp @@ -25,7 +25,7 @@ Function: memory_model_tsot::operator() void memory_model_tsot::operator()(symex_target_equationt &equation) { - print(8, "Adding TSO constraints"); + statistics() << "Adding TSO constraints" << eom; build_event_lists(equation); build_clock_type(equation); diff --git a/src/langapi/language_ui.cpp b/src/langapi/language_ui.cpp index 502bb932c60..9790a13f6b9 100644 --- a/src/langapi/language_ui.cpp +++ b/src/langapi/language_ui.cpp @@ -115,7 +115,10 @@ bool language_uit::parse(const std::string &filename) if(lf.language==NULL) { - error("failed to figure out type of file", filename); + source_locationt location; + location.set_file(filename); + error().source_location=location; + error() << "failed to figure out type of file" << eom; return true; } diff --git a/src/solvers/prop/prop_conv.cpp b/src/solvers/prop/prop_conv.cpp index 7e8207f4d09..e2958953c42 100644 --- a/src/solvers/prop/prop_conv.cpp +++ b/src/solvers/prop/prop_conv.cpp @@ -624,9 +624,7 @@ void prop_conv_solvert::ignoring(const exprt &expr) { // fall through - std::string msg="warning: ignoring "+expr.pretty(); - - print(2, msg); + warning() << "warning: ignoring " << expr.pretty() << eom; } /*******************************************************************\ @@ -662,12 +660,12 @@ decision_proceduret::resultt prop_conv_solvert::dec_solve() // post-processing isn't incremental yet if(!post_processing_done) { - print(8, "Post-processing"); + statistics() << "Post-processing" << eom; post_process(); post_processing_done=true; } - print(7, "Solving with "+prop.solver_text()); + statistics() << "Solving with " << prop.solver_text() << eom; propt::resultt result=prop.prop_solve(); diff --git a/src/solvers/sat/pbs_dimacs_cnf.cpp b/src/solvers/sat/pbs_dimacs_cnf.cpp index 5c45f8e0a09..cd2f04039bb 100644 --- a/src/solvers/sat/pbs_dimacs_cnf.cpp +++ b/src/solvers/sat/pbs_dimacs_cnf.cpp @@ -190,7 +190,8 @@ bool pbs_dimacs_cnft::pbs_solve() // print(line); if(strstr(line.c_str(), "time out")!=NULL) { - print(6, "WARNING: TIMED OUT. SOLUTION MAY BE INCORRECT.\n"); + status() << "WARNING: TIMED OUT. SOLUTION MAY BE INCORRECT." + << eom; return satisfied; } sscanf(line.c_str(), "%*s %*s %*s %d", &opt_sum); diff --git a/src/util/cout_message.cpp b/src/util/cout_message.cpp index a25be15e656..c709999c662 100644 --- a/src/util/cout_message.cpp +++ b/src/util/cout_message.cpp @@ -190,9 +190,9 @@ void gcc_message_handlert::print( else dest+=id2string(column)+": "; - if(level==message_clientt::M_ERROR) + if(level==messaget::M_ERROR) dest+="error: "; - else if(level==message_clientt::M_WARNING) + else if(level==messaget::M_WARNING) dest+="warning: "; } diff --git a/src/util/message.cpp b/src/util/message.cpp index 0fe90c1239b..0033395cc9e 100644 --- a/src/util/message.cpp +++ b/src/util/message.cpp @@ -88,7 +88,7 @@ void message_handlert::print( /*******************************************************************\ -Function: messaget::print +Function: messaget::~messaget Inputs: @@ -98,65 +98,6 @@ Function: messaget::print \*******************************************************************/ -void messaget::print(unsigned level, const std::string &message) +messaget::~messaget() { - if(message_handler!=NULL) - message_handler->print(level, message); -} - -/*******************************************************************\ - -Function: messaget::print - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -void messaget::print( - unsigned level, - const std::string &message, - int sequence_number, - const source_locationt &location) -{ - if(message_handler!=NULL) - message_handler->print(level, message, sequence_number, - location); -} - -/*******************************************************************\ - -Function: message_clientt::~message_clientt - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -message_clientt::~message_clientt() -{ -} - -/*******************************************************************\ - -Function: message_clientt::set_message_handler - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -void message_clientt::set_message_handler( - message_handlert &_message_handler) -{ - message_handler=&_message_handler; } diff --git a/src/util/message.h b/src/util/message.h index 5e902409e5a..8497c206d83 100644 --- a/src/util/message.h +++ b/src/util/message.h @@ -42,7 +42,7 @@ class message_handlert void set_verbosity(unsigned _verbosity) { verbosity=_verbosity; } unsigned get_verbosity() const { return verbosity; } - inline unsigned get_message_count(unsigned level) const + unsigned get_message_count(unsigned level) const { if(level>=message_count.size()) return 0; @@ -97,7 +97,7 @@ class stream_message_handlert:public message_handlert std::ostream &out; }; -class message_clientt +class messaget { public: // Standard message levels: @@ -117,17 +117,9 @@ class message_clientt M_STATISTICS=8, M_PROGRESS=9, M_DEBUG=10 }; - virtual ~message_clientt(); - - virtual void set_message_handler(message_handlert &_message_handler); - - message_clientt():message_handler(NULL) - { - } - - explicit message_clientt(message_handlert &_message_handler): - message_handler(&_message_handler) + virtual void set_message_handler(message_handlert &_message_handler) { + message_handler=&_message_handler; } message_handlert &get_message_handler() @@ -135,62 +127,27 @@ class message_clientt return *message_handler; } -protected: - message_handlert *message_handler; -}; - -class messaget:public message_clientt -{ -public: // constructors, destructor messaget(): + message_handler(NULL), mstream(M_DEBUG, *this) { } messaget(const messaget &other): - message_clientt(other), - mstream(M_DEBUG, *this) + message_handler(other.message_handler), + mstream(other.mstream) { } explicit messaget(message_handlert &_message_handler): - message_clientt(_message_handler), + message_handler(&_message_handler), mstream(M_DEBUG, *this) { } - virtual ~messaget() { } - - // old interface, will go away - void status( - const std::string &message, - const std::string &file) - { - source_locationt location; - location.set_file(file); - print(6, message, -1, location); - } - - void error( - const std::string &message, - const std::string &file) - { - source_locationt location; - location.set_file(file); - print(1, message, -1, location); - } - - virtual void print(unsigned level, const std::string &message); - - virtual void print( - unsigned level, - const std::string &message, - int sequence_number, // -1: no sequence information - const source_locationt &location); - - // New interface + virtual ~messaget(); class mstreamt:public std::ostringstream { @@ -203,6 +160,13 @@ class messaget:public message_clientt { } + mstreamt(const mstreamt &other): + message_level(other.message_level), + message(other.message), + source_location(other.source_location) + { + } + unsigned message_level; messaget &message; source_locationt source_location; @@ -223,7 +187,7 @@ class messaget:public message_clientt // Feeding 'eom' into the stream triggers // the printing of the message - static inline mstreamt &eom(mstreamt &m) + static mstreamt &eom(mstreamt &m) { if(m.message.message_handler) { @@ -241,61 +205,55 @@ class messaget:public message_clientt } // in lieu of std::endl - static inline mstreamt &endl(mstreamt &m) + static mstreamt &endl(mstreamt &m) { static_cast(m) << std::endl; return m; } - mstreamt &error() + mstreamt &get_mstream(unsigned message_level) { - mstream.message_level=M_ERROR; + mstream.message_level=message_level; return mstream; } + mstreamt &error() + { + return get_mstream(M_ERROR); + } + mstreamt &warning() { - mstream.message_level=M_WARNING; - return mstream; + return get_mstream(M_WARNING); } mstreamt &result() { - mstream.message_level=M_RESULT; - return mstream; + return get_mstream(M_RESULT); } mstreamt &status() { - mstream.message_level=M_STATUS; - return mstream; + return get_mstream(M_STATUS); } mstreamt &statistics() { - mstream.message_level=M_STATISTICS; - return mstream; + return get_mstream(M_STATISTICS); } mstreamt &progress() { - mstream.message_level=M_PROGRESS; - return mstream; + return get_mstream(M_PROGRESS); } mstreamt &debug() { - mstream.message_level=M_DEBUG; - return mstream; - } - - mstreamt &get_mstream(unsigned message_level) - { - mstream.message_level=message_level; - return mstream; + return get_mstream(M_DEBUG); } protected: + message_handlert *message_handler; mstreamt mstream; }; diff --git a/src/util/parser.cpp b/src/util/parser.cpp index 539ed1f0e63..579dea6fd27 100644 --- a/src/util/parser.cpp +++ b/src/util/parser.cpp @@ -63,6 +63,7 @@ void parsert::parse_error( tmp_source_location.set_column(column-before.size()); print(1, tmp, -1, tmp_source_location); #else - print(1, tmp, -1, source_location); + error().source_location=source_location; + error() << tmp << eom; #endif } From 9e25eb4e09f05b31a898e7ce61f77e7432ed1c46 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 7 Jul 2016 09:57:47 +0200 Subject: [PATCH 6/7] Make goto-cc fail when warnings are emitted and -Werror and -Wextra are set For goto-cl, goto-armcc, etc the equivalent options enable fail-on-warnings mode. Do not fail with -Werror -Wall (but not -Wextra) as that breaks too many builds as we don't have an equivalent of -Wno-... --- src/goto-cc/armcc_mode.cpp | 2 +- src/goto-cc/as_mode.cpp | 2 +- src/goto-cc/compile.cpp | 21 ++++++++++++++------- src/goto-cc/compile.h | 3 ++- src/goto-cc/cw_mode.cpp | 2 +- src/goto-cc/gcc_mode.cpp | 7 +++++-- src/goto-cc/ms_cl_mode.cpp | 2 +- 7 files changed, 25 insertions(+), 14 deletions(-) diff --git a/src/goto-cc/armcc_mode.cpp b/src/goto-cc/armcc_mode.cpp index b6b801059c8..e0a27b00d3e 100644 --- a/src/goto-cc/armcc_mode.cpp +++ b/src/goto-cc/armcc_mode.cpp @@ -46,7 +46,7 @@ int armcc_modet::doit() unsigned int verbosity=1; - compilet compiler(cmdline); + compilet compiler(cmdline, cmdline.isset("diag_error=")); #if 0 bool act_as_ld= diff --git a/src/goto-cc/as_mode.cpp b/src/goto-cc/as_mode.cpp index f2dd4be23d3..dc668522131 100644 --- a/src/goto-cc/as_mode.cpp +++ b/src/goto-cc/as_mode.cpp @@ -159,7 +159,7 @@ int as_modet::doit() config.set(cmdline); // determine actions to be undertaken - compilet compiler(cmdline); + compilet compiler(cmdline, cmdline.isset("fatal-warnings")); compiler.ui_message_handler.set_verbosity(verbosity); if(cmdline.isset('b')) // as86 only diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp index fae6623aaf1..3e858c34641 100644 --- a/src/goto-cc/compile.cpp +++ b/src/goto-cc/compile.cpp @@ -121,6 +121,9 @@ bool compilet::doit() return true; } + const unsigned warnings_before= + get_message_handler().get_message_count(messaget::M_WARNING); + if(source_files.size()>0) if(compile()) return true; @@ -133,7 +136,10 @@ bool compilet::doit() return true; } - return false; + return + warning_is_fatal && + get_message_handler().get_message_count(messaget::M_WARNING)!= + warnings_before; } /*******************************************************************\ @@ -156,8 +162,8 @@ bool compilet::add_input_file(const std::string &file_name) std::ifstream in(file_name); if(!in) { - error() << "failed to open file `" << file_name << "'" << eom; - return false; // generously ignore + warning() << "failed to open file `" << file_name << "'" << eom; + return warning_is_fatal; // generously ignore unless -Werror } } @@ -168,7 +174,7 @@ bool compilet::add_input_file(const std::string &file_name) // a file without extension; will ignore warning() << "input file `" << file_name << "' has no extension, not considered" << eom; - return false; + return warning_is_fatal; } std::string ext = file_name.substr(r+1, file_name.length()); @@ -329,7 +335,7 @@ bool compilet::find_library(const std::string &name) else if(is_elf_file(libname)) { warning() << "Warning: Cannot read ELF library " << libname << eom; - return false; + return warning_is_fatal; } } } @@ -752,11 +758,12 @@ Function: compilet::compilet \*******************************************************************/ -compilet::compilet(cmdlinet &_cmdline): +compilet::compilet(cmdlinet &_cmdline, bool Werror): language_uit(_cmdline, ui_message_handler), ui_message_handler(_cmdline, "goto-cc " CBMC_VERSION), ns(symbol_table), - cmdline(_cmdline) + cmdline(_cmdline), + warning_is_fatal(Werror) { mode=COMPILE_LINK_EXECUTABLE; echo_file_name=false; diff --git a/src/goto-cc/compile.h b/src/goto-cc/compile.h index 936f4cd21d5..c06ec1f3f0c 100644 --- a/src/goto-cc/compile.h +++ b/src/goto-cc/compile.h @@ -45,7 +45,7 @@ class compilet:public language_uit std::string object_file_extension; std::string output_file_object, output_file_executable; - explicit compilet(cmdlinet &_cmdline); + compilet(cmdlinet &_cmdline, bool Werror); ~compilet(); @@ -72,6 +72,7 @@ class compilet:public language_uit protected: cmdlinet &cmdline; + bool warning_is_fatal; unsigned function_body_count(const goto_functionst &); diff --git a/src/goto-cc/cw_mode.cpp b/src/goto-cc/cw_mode.cpp index ce4b65e4645..9ec578d9c57 100644 --- a/src/goto-cc/cw_mode.cpp +++ b/src/goto-cc/cw_mode.cpp @@ -46,7 +46,7 @@ int cw_modet::doit() unsigned int verbosity=1; - compilet compiler(cmdline); + compilet compiler(cmdline, cmdline.isset("Werror")); #if 0 bool act_as_ld= diff --git a/src/goto-cc/gcc_mode.cpp b/src/goto-cc/gcc_mode.cpp index 81c75d5c3bf..ede6bb55646 100644 --- a/src/goto-cc/gcc_mode.cpp +++ b/src/goto-cc/gcc_mode.cpp @@ -218,7 +218,7 @@ int gcc_modet::doit() return EX_OK; } - if(cmdline.isset("Wall")) + if(cmdline.isset("Wall") || cmdline.isset("Wextra")) verbosity=2; if(cmdline.isset("verbosity")) @@ -303,7 +303,10 @@ int gcc_modet::doit() config.ansi_c.double_width=config.ansi_c.single_width; // determine actions to be undertaken - compilet compiler(cmdline); + compilet compiler(cmdline, + cmdline.isset("Werror") && + cmdline.isset("Wextra") && + !cmdline.isset("Wno-error")); compiler.set_message_handler(get_message_handler()); if(act_as_ld) diff --git a/src/goto-cc/ms_cl_mode.cpp b/src/goto-cc/ms_cl_mode.cpp index c452c374be6..9a150d67527 100644 --- a/src/goto-cc/ms_cl_mode.cpp +++ b/src/goto-cc/ms_cl_mode.cpp @@ -59,7 +59,7 @@ int ms_cl_modet::doit() unsigned int verbosity=1; - compilet compiler(cmdline); + compilet compiler(cmdline, cmdline.isset("WX")); #if 0 bool act_as_ld= From c183996256f03715e216a8efe718bf7157d64242 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 28 Apr 2017 15:07:46 +0100 Subject: [PATCH 7/7] Pass message handler on to compilet GOTO conversion must honour the message handler set up by the chosen goto-cc mode. Thus the message handler set up in the specific mode has to be handed on to compilet. As a language_uit this requires a ui_message_handlert. Consequently make console_message_handlert, gcc_message_handlert ui_message_handlert in PLAIN ui mode (which is consistent). --- regression/ansi-c/message_handling1/main.c | 9 +++++++++ regression/ansi-c/message_handling1/test.desc | 7 +++++++ src/goto-cc/armcc_mode.cpp | 2 +- src/goto-cc/as_mode.cpp | 3 +-- src/goto-cc/compile.cpp | 9 ++++----- src/goto-cc/compile.h | 3 +-- src/goto-cc/cw_mode.cpp | 2 +- src/goto-cc/gcc_mode.cpp | 2 +- src/goto-cc/ms_cl_mode.cpp | 2 +- src/langapi/language_ui.cpp | 4 ++-- src/langapi/language_ui.h | 3 +-- src/util/cout_message.h | 6 +++--- src/util/ui_message.h | 4 ++++ 13 files changed, 36 insertions(+), 20 deletions(-) create mode 100644 regression/ansi-c/message_handling1/main.c create mode 100644 regression/ansi-c/message_handling1/test.desc diff --git a/regression/ansi-c/message_handling1/main.c b/regression/ansi-c/message_handling1/main.c new file mode 100644 index 00000000000..00193b44b77 --- /dev/null +++ b/regression/ansi-c/message_handling1/main.c @@ -0,0 +1,9 @@ +int main() +{ + goto bla; + + for(int i=0; i<5; ++i) + { +bla: i=10; + } +} diff --git a/regression/ansi-c/message_handling1/test.desc b/regression/ansi-c/message_handling1/test.desc new file mode 100644 index 00000000000..277edf65161 --- /dev/null +++ b/regression/ansi-c/message_handling1/test.desc @@ -0,0 +1,7 @@ +CORE +main.c +--verbosity 2 +^EXIT=0$ +^SIGNAL=0$ +-- +encountered goto `bla' that enters one or more lexical blocks diff --git a/src/goto-cc/armcc_mode.cpp b/src/goto-cc/armcc_mode.cpp index e0a27b00d3e..df5e2001237 100644 --- a/src/goto-cc/armcc_mode.cpp +++ b/src/goto-cc/armcc_mode.cpp @@ -46,7 +46,7 @@ int armcc_modet::doit() unsigned int verbosity=1; - compilet compiler(cmdline, cmdline.isset("diag_error=")); + compilet compiler(cmdline, message_handler, cmdline.isset("diag_error=")); #if 0 bool act_as_ld= diff --git a/src/goto-cc/as_mode.cpp b/src/goto-cc/as_mode.cpp index dc668522131..0f4fbf72fae 100644 --- a/src/goto-cc/as_mode.cpp +++ b/src/goto-cc/as_mode.cpp @@ -159,8 +159,7 @@ int as_modet::doit() config.set(cmdline); // determine actions to be undertaken - compilet compiler(cmdline, cmdline.isset("fatal-warnings")); - compiler.ui_message_handler.set_verbosity(verbosity); + compilet compiler(cmdline, message_handler, cmdline.isset("fatal-warnings")); if(cmdline.isset('b')) // as86 only { diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp index 3e858c34641..5b91efdeb47 100644 --- a/src/goto-cc/compile.cpp +++ b/src/goto-cc/compile.cpp @@ -415,7 +415,7 @@ bool compilet::link() symbol_table.remove(goto_functionst::entry_point()); compiled_functions.function_map.erase(goto_functionst::entry_point()); - if(ansi_c_entry_point(symbol_table, "main", ui_message_handler)) + if(ansi_c_entry_point(symbol_table, "main", get_message_handler())) return true; // entry_point may (should) add some more functions. @@ -758,9 +758,8 @@ Function: compilet::compilet \*******************************************************************/ -compilet::compilet(cmdlinet &_cmdline, bool Werror): - language_uit(_cmdline, ui_message_handler), - ui_message_handler(_cmdline, "goto-cc " CBMC_VERSION), +compilet::compilet(cmdlinet &_cmdline, ui_message_handlert &mh, bool Werror): + language_uit(_cmdline, mh), ns(symbol_table), cmdline(_cmdline), warning_is_fatal(Werror) @@ -849,7 +848,7 @@ Function: compilet::convert_symbols void compilet::convert_symbols(goto_functionst &dest) { - goto_convert_functionst converter(symbol_table, dest, ui_message_handler); + goto_convert_functionst converter(symbol_table, dest, get_message_handler()); // the compilation may add symbols! diff --git a/src/goto-cc/compile.h b/src/goto-cc/compile.h index c06ec1f3f0c..37344935b33 100644 --- a/src/goto-cc/compile.h +++ b/src/goto-cc/compile.h @@ -20,7 +20,6 @@ Date: June 2006 class compilet:public language_uit { public: - ui_message_handlert ui_message_handler; namespacet ns; goto_functionst compiled_functions; bool echo_file_name; @@ -45,7 +44,7 @@ class compilet:public language_uit std::string object_file_extension; std::string output_file_object, output_file_executable; - compilet(cmdlinet &_cmdline, bool Werror); + compilet(cmdlinet &_cmdline, ui_message_handlert &mh, bool Werror); ~compilet(); diff --git a/src/goto-cc/cw_mode.cpp b/src/goto-cc/cw_mode.cpp index 9ec578d9c57..9ee04df633a 100644 --- a/src/goto-cc/cw_mode.cpp +++ b/src/goto-cc/cw_mode.cpp @@ -46,7 +46,7 @@ int cw_modet::doit() unsigned int verbosity=1; - compilet compiler(cmdline, cmdline.isset("Werror")); + compilet compiler(cmdline, message_handler, cmdline.isset("Werror")); #if 0 bool act_as_ld= diff --git a/src/goto-cc/gcc_mode.cpp b/src/goto-cc/gcc_mode.cpp index ede6bb55646..bbae0bcf009 100644 --- a/src/goto-cc/gcc_mode.cpp +++ b/src/goto-cc/gcc_mode.cpp @@ -304,10 +304,10 @@ int gcc_modet::doit() // determine actions to be undertaken compilet compiler(cmdline, + gcc_message_handler, cmdline.isset("Werror") && cmdline.isset("Wextra") && !cmdline.isset("Wno-error")); - compiler.set_message_handler(get_message_handler()); if(act_as_ld) compiler.mode=compilet::LINK_LIBRARY; diff --git a/src/goto-cc/ms_cl_mode.cpp b/src/goto-cc/ms_cl_mode.cpp index 9a150d67527..20f4be66e28 100644 --- a/src/goto-cc/ms_cl_mode.cpp +++ b/src/goto-cc/ms_cl_mode.cpp @@ -59,7 +59,7 @@ int ms_cl_modet::doit() unsigned int verbosity=1; - compilet compiler(cmdline, cmdline.isset("WX")); + compilet compiler(cmdline, message_handler, cmdline.isset("WX")); #if 0 bool act_as_ld= diff --git a/src/langapi/language_ui.cpp b/src/langapi/language_ui.cpp index 9790a13f6b9..70853be9e6b 100644 --- a/src/langapi/language_ui.cpp +++ b/src/langapi/language_ui.cpp @@ -33,8 +33,8 @@ Function: language_uit::language_uit language_uit::language_uit( const cmdlinet &cmdline, ui_message_handlert &_ui_message_handler): - ui_message_handler(_ui_message_handler), - _cmdline(cmdline) + _cmdline(cmdline), + ui_message_handler(_ui_message_handler) { set_message_handler(ui_message_handler); } diff --git a/src/langapi/language_ui.h b/src/langapi/language_ui.h index b82507f4c75..50c8311b714 100644 --- a/src/langapi/language_ui.h +++ b/src/langapi/language_ui.h @@ -48,10 +48,9 @@ class language_uit:public messaget return ui_message_handler.get_ui(); } - ui_message_handlert &ui_message_handler; - protected: const cmdlinet &_cmdline; + ui_message_handlert &ui_message_handler; }; #endif // CPROVER_LANGAPI_LANGUAGE_UI_H diff --git a/src/util/cout_message.h b/src/util/cout_message.h index 71f9ce83f4f..1f22e5c009c 100644 --- a/src/util/cout_message.h +++ b/src/util/cout_message.h @@ -9,7 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_UTIL_COUT_MESSAGE_H #define CPROVER_UTIL_COUT_MESSAGE_H -#include "message.h" +#include "ui_message.h" class cout_message_handlert:public stream_message_handlert { @@ -25,7 +25,7 @@ class cerr_message_handlert:public stream_message_handlert cerr_message_handlert(); }; -class console_message_handlert:public message_handlert +class console_message_handlert:public ui_message_handlert { public: // level 4 and upwards go to cout, level 1-3 to cerr @@ -36,7 +36,7 @@ class console_message_handlert:public message_handlert virtual void flush(unsigned level) override; }; -class gcc_message_handlert:public message_handlert +class gcc_message_handlert:public ui_message_handlert { public: // aims to imitate the messages gcc prints diff --git a/src/util/ui_message.h b/src/util/ui_message.h index c4e70e6b4cd..ea0c2dbc6e4 100644 --- a/src/util/ui_message.h +++ b/src/util/ui_message.h @@ -18,6 +18,10 @@ class ui_message_handlert:public message_handlert ui_message_handlert(uit, const std::string &program); ui_message_handlert(const class cmdlinet &, const std::string &program); + ui_message_handlert(): + _ui(uit::PLAIN) + { + } virtual ~ui_message_handlert();