diff --git a/src/util/cout_message.cpp b/src/util/cout_message.cpp index 9e264df0e37..7153b333922 100644 --- a/src/util/cout_message.cpp +++ b/src/util/cout_message.cpp @@ -100,7 +100,6 @@ void console_message_handlert::flush(unsigned level) void gcc_message_handlert::print( unsigned level, const std::string &message, - int, const source_locationt &location) { const irep_idt file=location.get_file(); diff --git a/src/util/cout_message.h b/src/util/cout_message.h index d17f67e3eec..4972a73bbb0 100644 --- a/src/util/cout_message.h +++ b/src/util/cout_message.h @@ -60,7 +60,6 @@ class gcc_message_handlert:public ui_message_handlert virtual void print( unsigned level, const std::string &message, - int sequence_number, const source_locationt &location) override; }; diff --git a/src/util/message.cpp b/src/util/message.cpp index 3e3ed886cba..0ea87e80786 100644 --- a/src/util/message.cpp +++ b/src/util/message.cpp @@ -14,7 +14,6 @@ Author: Daniel Kroening, kroening@kroening.com void message_handlert::print( unsigned level, const std::string &message, - int, const source_locationt &location) { std::string dest; @@ -92,7 +91,6 @@ unsigned messaget::eval_verbosity( messaget::M_WARNING, "verbosity value " + user_input + " out of range, using debug-level (" + std::to_string(messaget::M_DEBUG) + ") verbosity", - -1, source_locationt()); v = messaget::M_DEBUG; diff --git a/src/util/message.h b/src/util/message.h index 1e16ae1def9..18bb60fda95 100644 --- a/src/util/message.h +++ b/src/util/message.h @@ -50,7 +50,6 @@ class message_handlert virtual void print( unsigned level, const std::string &message, - int sequence_number, const source_locationt &location); virtual void flush(unsigned level) @@ -65,7 +64,7 @@ class message_handlert void set_verbosity(unsigned _verbosity) { verbosity=_verbosity; } unsigned get_verbosity() const { return verbosity; } - unsigned get_message_count(unsigned level) const + std::size_t get_message_count(unsigned level) const { if(level>=message_count.size()) return 0; @@ -75,7 +74,7 @@ class message_handlert protected: unsigned verbosity; - std::vector message_count; + std::vector message_count; }; class null_message_handlert:public message_handlert @@ -89,7 +88,6 @@ class null_message_handlert:public message_handlert virtual void print( unsigned level, const std::string &message, - int, const source_locationt &) { print(level, message); @@ -276,7 +274,6 @@ class messaget m.message.message_handler->print( m.message_level, m.str(), - -1, m.source_location); m.message.message_handler->flush(m.message_level); } diff --git a/src/util/ui_message.cpp b/src/util/ui_message.cpp index c6ab39f1022..48303308e9e 100644 --- a/src/util/ui_message.cpp +++ b/src/util/ui_message.cpp @@ -149,7 +149,7 @@ void ui_message_handlert::print( { source_locationt location; location.make_nil(); - print(level, message, -1, location); + print(level, message, location); if(always_flush) flush(level); } @@ -206,7 +206,6 @@ void ui_message_handlert::print( void ui_message_handlert::print( unsigned level, const std::string &message, - int sequence_number, const source_locationt &location) { message_handlert::print(level, message); @@ -217,7 +216,7 @@ void ui_message_handlert::print( { case uit::PLAIN: message_handlert::print( - level, message, sequence_number, location); + level, message, location); break; case uit::XML_UI: @@ -230,10 +229,7 @@ void ui_message_handlert::print( const char *type=level_string(level); - std::string sequence_number_str= - sequence_number>=0?std::to_string(sequence_number):""; - - ui_msg(type, tmp_message, sequence_number_str, location); + ui_msg(type, tmp_message, location); } break; } @@ -242,8 +238,7 @@ void ui_message_handlert::print( void ui_message_handlert::ui_msg( const std::string &type, - const std::string &msg1, - const std::string &msg2, + const std::string &msg, const source_locationt &location) { switch(get_ui()) @@ -252,11 +247,11 @@ void ui_message_handlert::ui_msg( break; case uit::XML_UI: - xml_ui_msg(type, msg1, msg2, location); + xml_ui_msg(type, msg, location); break; case uit::JSON_UI: - json_ui_msg(type, msg1, msg2, location); + json_ui_msg(type, msg, location); break; } } @@ -264,7 +259,6 @@ void ui_message_handlert::ui_msg( void ui_message_handlert::xml_ui_msg( const std::string &type, const std::string &msg1, - const std::string &, const source_locationt &location) { xmlt result; @@ -287,7 +281,6 @@ void ui_message_handlert::xml_ui_msg( void ui_message_handlert::json_ui_msg( const std::string &type, const std::string &msg1, - const std::string &, const source_locationt &location) { INVARIANT(json_stream, "JSON stream must be initialized before use"); diff --git a/src/util/ui_message.h b/src/util/ui_message.h index 06f458edc51..4a4fc104dd3 100644 --- a/src/util/ui_message.h +++ b/src/util/ui_message.h @@ -71,7 +71,6 @@ class ui_message_handlert : public message_handlert virtual void print( unsigned level, const std::string &message, - int sequence_number, const source_locationt &location) override; virtual void print( @@ -84,20 +83,17 @@ class ui_message_handlert : public message_handlert virtual void xml_ui_msg( const std::string &type, - const std::string &msg1, - const std::string &msg2, + const std::string &msg, const source_locationt &location); virtual void json_ui_msg( const std::string &type, - const std::string &msg1, - const std::string &msg2, + const std::string &msg, const source_locationt &location); virtual void ui_msg( const std::string &type, - const std::string &msg1, - const std::string &msg2, + const std::string &msg, const source_locationt &location); const char *level_string(unsigned level);