From 9395b51e89b3665b74b92cad3e323fd93982e58f Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 19 Mar 2024 12:20:34 +0000 Subject: [PATCH 1/2] Complexity limiter: remove default constructor This is never needed or used and would require default-constructing a messaget, which is no longer possible. --- src/goto-symex/complexity_limiter.h | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/goto-symex/complexity_limiter.h b/src/goto-symex/complexity_limiter.h index c893f330ed0..c29d6676287 100644 --- a/src/goto-symex/complexity_limiter.h +++ b/src/goto-symex/complexity_limiter.h @@ -48,8 +48,6 @@ class optionst; class complexity_limitert { public: - complexity_limitert() = default; - complexity_limitert(message_handlert &logger, const optionst &options); /// Is the complexity module active? From 8110e31ee8629a037bf761a3015287fcb041b904 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 20 Dec 2023 13:22:14 +0000 Subject: [PATCH 2/2] Remove deprecated messaget() constructor It is now no longer possible to construct a messaget object that is not fully configured, i.e., lacks a message handler. --- src/util/message.h | 14 +++----------- src/util/parser.h | 11 +---------- 2 files changed, 4 insertions(+), 21 deletions(-) diff --git a/src/util/message.h b/src/util/message.h index 23476ce4e9c..ec1624855e8 100644 --- a/src/util/message.h +++ b/src/util/message.h @@ -10,15 +10,14 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_UTIL_MESSAGE_H #define CPROVER_UTIL_MESSAGE_H +#include "invariant.h" +#include "source_location.h" + #include #include #include #include -#include "deprecate.h" -#include "invariant.h" -#include "source_location.h" - class json_objectt; class jsont; class structured_datat; @@ -191,13 +190,6 @@ class messaget // constructors, destructor - DEPRECATED(SINCE(2019, 1, 7, "use messaget(message_handler) instead")) - messaget(): - message_handler(nullptr), - mstream(M_DEBUG, *this) - { - } - messaget(const messaget &other): message_handler(other.message_handler), mstream(other.mstream, *this) diff --git a/src/util/parser.h b/src/util/parser.h index 767162d1800..32412d3226d 100644 --- a/src/util/parser.h +++ b/src/util/parser.h @@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_UTIL_PARSER_H #define CPROVER_UTIL_PARSER_H -#include "deprecate.h" #include "expr.h" #include "message.h" @@ -30,11 +29,6 @@ class parsert std::vector stack; - DEPRECATED(SINCE(2023, 12, 20, "use parsert(message_handler) instead")) - parsert() : in(nullptr), line_no(0), previous_line_no(0), column(1) - { - } - explicit parsert(message_handlert &message_handler) : in(nullptr), log(message_handler), @@ -135,11 +129,8 @@ class parsert column+=token_width; } - // should be protected or even just be a reference to a message handler, but - // for now enables a step-by-step transition - messaget log; - protected: + messaget log; source_locationt source_location; unsigned line_no, previous_line_no; unsigned column;