From aa47f32aaff51c6ea685c9f23d85529f95d18e68 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 20 Dec 2023 13:34:12 +0000
Subject: [PATCH 01/16] C++ front-end: configure C++11+ syntax without
 ansi_c_parser object

There is no need to access the parser object when the same information
is available directly from `config`.
---
 src/cpp/parse.cpp | 32 +++++++++++++++++---------------
 1 file changed, 17 insertions(+), 15 deletions(-)

diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp
index c16a92a6d12..a0ce60aca87 100644
--- a/src/cpp/parse.cpp
+++ b/src/cpp/parse.cpp
@@ -195,10 +195,14 @@ void new_scopet::print_rec(std::ostream &out, unsigned indent) const
 class Parser // NOLINT(readability/identifiers)
 {
 public:
-  explicit Parser(cpp_parsert &_cpp_parser):
-    lex(_cpp_parser.token_buffer),
-    parser(_cpp_parser),
-    max_errors(10)
+  explicit Parser(cpp_parsert &_cpp_parser)
+    : lex(_cpp_parser.token_buffer),
+      parser(_cpp_parser),
+      max_errors(10),
+      cpp11(
+        config.cpp.cpp_standard == configt::cppt::cpp_standardt::CPP11 ||
+        config.cpp.cpp_standard == configt::cppt::cpp_standardt::CPP14 ||
+        config.cpp.cpp_standard == configt::cppt::cpp_standardt::CPP17)
   {
     root_scope.kind=new_scopet::kindt::NAMESPACE;
     current_scope=&root_scope;
@@ -408,6 +412,7 @@ class Parser // NOLINT(readability/identifiers)
   }
 
   unsigned int max_errors;
+  const bool cpp11;
 };
 
 static bool is_identifier(int token)
@@ -1986,13 +1991,10 @@ bool Parser::optStorageSpec(cpp_storage_spect &storage_spec)
 {
   int t=lex.LookAhead(0);
 
-  if(t==TOK_STATIC ||
-     t==TOK_EXTERN ||
-     (t == TOK_AUTO && !ansi_c_parser.cpp11) ||
-     t==TOK_REGISTER ||
-     t==TOK_MUTABLE ||
-     t==TOK_GCC_ASM ||
-     t==TOK_THREAD_LOCAL)
+  if(
+    t == TOK_STATIC || t == TOK_EXTERN || (t == TOK_AUTO && !cpp11) ||
+    t == TOK_REGISTER || t == TOK_MUTABLE || t == TOK_GCC_ASM ||
+    t == TOK_THREAD_LOCAL)
   {
     cpp_tokent tk;
     lex.get_token(tk);
@@ -2730,7 +2732,7 @@ bool Parser::rConstructorDecl(
 
     case TOK_DEFAULT: // C++0x
       {
-        if(!ansi_c_parser.cpp11)
+        if(!cpp11)
         {
           SyntaxError();
           return false;
@@ -2743,7 +2745,7 @@ bool Parser::rConstructorDecl(
 
     case TOK_DELETE: // C++0x
       {
-        if(!ansi_c_parser.cpp11)
+        if(!cpp11)
         {
           SyntaxError();
           return false;
@@ -2907,7 +2909,7 @@ bool Parser::rDeclaratorWithInit(
 
       if(lex.LookAhead(0)==TOK_DEFAULT) // C++0x
       {
-        if(!ansi_c_parser.cpp11)
+        if(!cpp11)
         {
           SyntaxError();
           return false;
@@ -2919,7 +2921,7 @@ bool Parser::rDeclaratorWithInit(
       }
       else if(lex.LookAhead(0)==TOK_DELETE) // C++0x
       {
-        if(!ansi_c_parser.cpp11)
+        if(!cpp11)
         {
           SyntaxError();
           return false;

From 6f2fd347f8199b7cddfe7fcc14a3e29f3ba95cdd Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 20 Dec 2023 13:28:01 +0000
Subject: [PATCH 02/16] Make ansi_c_internal_additions independent of the
 parser object

Thread through a Boolean flag rather than relying on the parser object
far away from the actual parser.
---
 src/ansi-c/ansi_c_internal_additions.cpp |  8 ++++----
 src/ansi-c/ansi_c_internal_additions.h   |  4 +++-
 src/ansi-c/ansi_c_language.cpp           |  2 +-
 src/ansi-c/builtin_factory.cpp           |  3 ++-
 src/ansi-c/builtin_factory.h             |  1 +
 src/ansi-c/c_typecheck_base.h            |  2 ++
 src/ansi-c/c_typecheck_expr.cpp          | 11 ++++++++++-
 src/cpp/cpp_typecheck.cpp                |  3 ++-
 src/cpp/cpp_typecheck.h                  |  2 +-
 9 files changed, 26 insertions(+), 10 deletions(-)

diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp
index 749353af3ce..e3eaa05834e 100644
--- a/src/ansi-c/ansi_c_internal_additions.cpp
+++ b/src/ansi-c/ansi_c_internal_additions.cpp
@@ -158,7 +158,9 @@ max_malloc_size(std::size_t pointer_width, std::size_t object_bits)
   return ((mp_integer)1) << (mp_integer)bits_for_positive_offset;
 }
 
-void ansi_c_internal_additions(std::string &code)
+void ansi_c_internal_additions(
+  std::string &code,
+  bool support_ts_18661_3_Floatn_types)
 {
   // clang-format off
   // do the built-in types and variables
@@ -247,9 +249,7 @@ void ansi_c_internal_additions(std::string &code)
     config.ansi_c.mode == configt::ansi_ct::flavourt::ARM)
   {
     code+=gcc_builtin_headers_types;
-    // check the parser and not config.ansi_c.ts_18661_3_Floatn_types to adjust
-    // behaviour depending on C or C++ context
-    if(ansi_c_parser.ts_18661_3_Floatn_types)
+    if(support_ts_18661_3_Floatn_types)
       code += gcc_builtin_headers_types_gcc7plus;
 
     // there are many more, e.g., look at
diff --git a/src/ansi-c/ansi_c_internal_additions.h b/src/ansi-c/ansi_c_internal_additions.h
index 735022d6703..c2531b65337 100644
--- a/src/ansi-c/ansi_c_internal_additions.h
+++ b/src/ansi-c/ansi_c_internal_additions.h
@@ -12,7 +12,9 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <string>
 
-void ansi_c_internal_additions(std::string &code);
+void ansi_c_internal_additions(
+  std::string &code,
+  bool support_ts_18661_3_Floatn_types);
 void ansi_c_architecture_strings(std::string &code);
 
 extern const char clang_builtin_headers[];
diff --git a/src/ansi-c/ansi_c_language.cpp b/src/ansi-c/ansi_c_language.cpp
index af29ed2599e..c4eb9cadc14 100644
--- a/src/ansi-c/ansi_c_language.cpp
+++ b/src/ansi-c/ansi_c_language.cpp
@@ -68,7 +68,7 @@ bool ansi_c_languaget::parse(
   // parsing
 
   std::string code;
-  ansi_c_internal_additions(code);
+  ansi_c_internal_additions(code, config.ansi_c.ts_18661_3_Floatn_types);
   std::istringstream codestr(code);
 
   ansi_c_parser.clear();
diff --git a/src/ansi-c/builtin_factory.cpp b/src/ansi-c/builtin_factory.cpp
index 0d9de3c48cd..bfed926cb03 100644
--- a/src/ansi-c/builtin_factory.cpp
+++ b/src/ansi-c/builtin_factory.cpp
@@ -97,6 +97,7 @@ static bool convert(
 //! \return 'true' on error
 bool builtin_factory(
   const irep_idt &identifier,
+  bool support_ts_18661_3_Floatn_types,
   symbol_table_baset &symbol_table,
   message_handlert &mh)
 {
@@ -106,7 +107,7 @@ bool builtin_factory(
   std::ostringstream s;
 
   std::string code;
-  ansi_c_internal_additions(code);
+  ansi_c_internal_additions(code, support_ts_18661_3_Floatn_types);
   s << code;
 
   // our own extensions
diff --git a/src/ansi-c/builtin_factory.h b/src/ansi-c/builtin_factory.h
index 8a012894c3f..e270d4917f1 100644
--- a/src/ansi-c/builtin_factory.h
+++ b/src/ansi-c/builtin_factory.h
@@ -17,6 +17,7 @@ class symbol_table_baset;
 //! \return 'true' in case of error
 bool builtin_factory(
   const irep_idt &identifier,
+  bool support_ts_18661_3_Floatn_types,
   symbol_table_baset &,
   message_handlert &);
 
diff --git a/src/ansi-c/c_typecheck_base.h b/src/ansi-c/c_typecheck_base.h
index bbe4948376e..dc0b11a209a 100644
--- a/src/ansi-c/c_typecheck_base.h
+++ b/src/ansi-c/c_typecheck_base.h
@@ -250,6 +250,8 @@ class c_typecheck_baset:
 
   virtual bool gcc_types_compatible_p(const typet &, const typet &);
 
+  virtual bool builtin_factory(const irep_idt &);
+
   // types
   virtual void typecheck_type(typet &type);
   virtual void typecheck_compound_type(struct_union_typet &type);
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index df210afc6cf..1879b6a8dc2 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/src/ansi-c/c_typecheck_expr.cpp
@@ -2072,6 +2072,15 @@ void c_typecheck_baset::typecheck_obeys_contract_call(
   expr.type() = bool_typet();
 }
 
+bool c_typecheck_baset::builtin_factory(const irep_idt &identifier)
+{
+  return ::builtin_factory(
+    identifier,
+    config.ansi_c.ts_18661_3_Floatn_types,
+    symbol_table,
+    get_message_handler());
+}
+
 void c_typecheck_baset::typecheck_side_effect_function_call(
   side_effect_expr_function_callt &expr)
 {
@@ -2106,7 +2115,7 @@ void c_typecheck_baset::typecheck_side_effect_function_call(
         typecheck_typed_target_call(expr);
       }
       // Is this a builtin?
-      else if(!builtin_factory(identifier, symbol_table, get_message_handler()))
+      else if(!builtin_factory(identifier))
       {
         // yes, it's a builtin
       }
diff --git a/src/cpp/cpp_typecheck.cpp b/src/cpp/cpp_typecheck.cpp
index 06f6f69009b..6f888c1cb79 100644
--- a/src/cpp/cpp_typecheck.cpp
+++ b/src/cpp/cpp_typecheck.cpp
@@ -325,7 +325,8 @@ void cpp_typecheckt::clean_up()
 
 bool cpp_typecheckt::builtin_factory(const irep_idt &identifier)
 {
-  return ::builtin_factory(identifier, symbol_table, get_message_handler());
+  return ::builtin_factory(
+    identifier, false, symbol_table, get_message_handler());
 }
 
 bool cpp_typecheckt::contains_cpp_name(const exprt &expr)
diff --git a/src/cpp/cpp_typecheck.h b/src/cpp/cpp_typecheck.h
index 814b3d8c13e..0e64a2f38cb 100644
--- a/src/cpp/cpp_typecheck.h
+++ b/src/cpp/cpp_typecheck.h
@@ -343,7 +343,7 @@ class cpp_typecheckt:public c_typecheck_baset
 
   void add_method_body(symbolt *_method_symbol);
 
-  bool builtin_factory(const irep_idt &);
+  bool builtin_factory(const irep_idt &) override;
 
   // types
 

From d2ca83bd4444f67ea71d8254ecb3e56a056686f2 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 20 Dec 2023 09:26:40 +0000
Subject: [PATCH 03/16] Permit constructing parsert with a message handler

This is to provide a path to remove the long-deprecated messaget()
constructor. Uses of this new constructor will be added in separate
commits.
---
 src/util/parser.h | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/src/util/parser.h b/src/util/parser.h
index 70a796ec4a9..c19aeb58977 100644
--- a/src/util/parser.h
+++ b/src/util/parser.h
@@ -12,6 +12,7 @@ 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"
 
@@ -39,7 +40,13 @@ class parsert
     last_line.clear();
   }
 
+  DEPRECATED(SINCE(2023, 12, 20, "use parsert(message_handler) instead"))
   parsert():in(nullptr) { clear(); }
+  explicit parsert(message_handlert &message_handler)
+    : in(nullptr), log(message_handler)
+  {
+    clear();
+  }
   virtual ~parsert() { }
 
   // The following are for the benefit of the scanner

From eb4f6dc0a0354d1763903b03dae37d608e0dcb0d Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 20 Dec 2023 09:28:03 +0000
Subject: [PATCH 04/16] xml_parsert: construct with message handler

This both avoids an object of static lifetime as well as it fixes the
(transitive) use of the deprecated messaget() constructor.
---
 src/xmllang/parser.y       |  7 +++++--
 src/xmllang/scanner.l      | 20 ++++++++++++++++++--
 src/xmllang/xml_parser.cpp | 13 +++++++++----
 src/xmllang/xml_parser.h   | 19 +++++++++----------
 4 files changed, 41 insertions(+), 18 deletions(-)

diff --git a/src/xmllang/parser.y b/src/xmllang/parser.y
index 9e3e7ccc5db..44c330f3dfe 100644
--- a/src/xmllang/parser.y
+++ b/src/xmllang/parser.y
@@ -3,10 +3,10 @@
 
 #include "xml_parser.h"
 
-int yyxmllex();
+int yyxmllex(xml_parsert &xml_parser);
 extern char *yyxmltext;
 
-int yyxmlerror(const std::string &error)
+int yyxmlerror(xml_parsert &xml_parser, const std::string &error)
 {
   xml_parser.parse_error(error, yyxmltext);
   return 0;
@@ -26,6 +26,9 @@ int yyxmlerror(const std::string &error)
 #endif
 %}
 
+%parse-param {xml_parsert &xml_parser}
+%lex-param {xml_parsert &xml_parser}
+
 %union {char *s;}
 
 %token STARTXMLDECL
diff --git a/src/xmllang/scanner.l b/src/xmllang/scanner.l
index a9907847c58..8849bdf0c30 100755
--- a/src/xmllang/scanner.l
+++ b/src/xmllang/scanner.l
@@ -19,7 +19,7 @@
 #include "xml_parser.h"
 #include "xml_y.tab.h"
 
-#define PARSER xml_parser
+#define PARSER (*xml_parser)
 
 //static int keep;  /* To store start condition */
 
@@ -65,6 +65,22 @@ string     \"([^"&]|{esc})*\"|\'([^'&]|{esc})*\'
 %s PI
 %s DTD
 
+%{
+static xml_parsert *xml_parser;
+
+int yyxmllex(void);
+
+int yyxmllex(xml_parsert &_xml_parser)
+{
+  // our scanner is not reentrant
+  PRECONDITION(!xml_parser);
+  xml_parser = &_xml_parser;
+  int result = yyxmllex();
+  xml_parser = nullptr;
+  return result;
+}
+%}
+
 %%
 
 <INITIAL,PI>{ws}  {/* skip */}
@@ -87,7 +103,7 @@ string     \"([^"&]|{esc})*\"|\'([^'&]|{esc})*\'
 <DTD>.            {/* skip */}
 <DTD>\]{close}    {BEGIN(INITIAL); /* skip */}
 
-.                 { yyxmlerror("unexpected character"); }
+.                 { yyxmlerror(*xml_parser, "unexpected character"); }
 {nl}              {/* skip, must be an extra one at EOF */;}
 
 %%
diff --git a/src/xmllang/xml_parser.cpp b/src/xmllang/xml_parser.cpp
index ed1c2d113b9..097652b176e 100644
--- a/src/xmllang/xml_parser.cpp
+++ b/src/xmllang/xml_parser.cpp
@@ -10,7 +10,12 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <fstream>
 
-xml_parsert xml_parser;
+int yyxmlparse(xml_parsert &);
+
+bool xml_parsert::parse()
+{
+  return yyxmlparse(*this) != 0;
+}
 
 // 'do it all' function
 bool parse_xml(
@@ -19,12 +24,12 @@ bool parse_xml(
   message_handlert &message_handler,
   xmlt &dest)
 {
-  xml_parser.clear();
+  xml_parsert xml_parser{message_handler};
+
   xml_parser.set_file(filename);
   xml_parser.in=&in;
-  xml_parser.log.set_message_handler(message_handler);
 
-  bool result=yyxmlparse()!=0;
+  bool result = xml_parser.parse();
 
   // save result
   xml_parser.parse_tree.element.swap(dest);
diff --git a/src/xmllang/xml_parser.h b/src/xmllang/xml_parser.h
index f4659160653..5143259900e 100644
--- a/src/xmllang/xml_parser.h
+++ b/src/xmllang/xml_parser.h
@@ -14,11 +14,15 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "xml_parse_tree.h"
 
-int yyxmlparse();
-
 class xml_parsert:public parsert
 {
 public:
+  explicit xml_parsert(message_handlert &message_handler)
+    : parsert(message_handler)
+  {
+    stack.push_back(&parse_tree.element);
+  }
+
   xml_parse_treet parse_tree;
 
   std::list<xmlt *> stack;
@@ -28,10 +32,7 @@ class xml_parsert:public parsert
     return *stack.back();
   }
 
-  virtual bool parse()
-  {
-    return yyxmlparse()!=0;
-  }
+  bool parse() override;
 
   void new_level()
   {
@@ -39,7 +40,7 @@ class xml_parsert:public parsert
     stack.push_back(&current().elements.back());
   }
 
-  virtual void clear()
+  void clear() override
   {
     parse_tree.clear();
     // set up stack
@@ -48,9 +49,7 @@ class xml_parsert:public parsert
   }
 };
 
-extern xml_parsert xml_parser;
-
-int yyxmlerror(const std::string &error);
+int yyxmlerror(xml_parsert &xml_parser, const std::string &error);
 
 // 'do it all' functions
 bool parse_xml(

From 28bae14ad178c969a41e27c309b267eeb5278d40 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 20 Dec 2023 13:23:54 +0000
Subject: [PATCH 05/16] jsil_parsert: construct with message handler

This both avoids an object of static lifetime as well as it fixes the
(transitive) use of the deprecated messaget() constructor.
---
 src/jsil/jsil_language.cpp |  7 ++-----
 src/jsil/jsil_parser.cpp   | 10 ----------
 src/jsil/jsil_parser.h     | 17 ++++++++++-------
 src/jsil/parser.y          | 16 +++++++++++++++-
 src/jsil/scanner.l         | 20 +++++++++++---------
 5 files changed, 38 insertions(+), 32 deletions(-)

diff --git a/src/jsil/jsil_language.cpp b/src/jsil/jsil_language.cpp
index c363a5396e0..8b0d543c949 100644
--- a/src/jsil/jsil_language.cpp
+++ b/src/jsil/jsil_language.cpp
@@ -62,12 +62,11 @@ bool jsil_languaget::parse(
   parse_path=path;
 
   // parsing
+  jsil_parsert jsil_parser{message_handler};
   jsil_parser.clear();
   jsil_parser.set_file(path);
   jsil_parser.in=&instream;
-  jsil_parser.log.set_message_handler(message_handler);
 
-  jsil_scanner_init();
   bool result=jsil_parser.parse();
 
   // save result
@@ -137,12 +136,10 @@ bool jsil_languaget::to_expr(
   std::istringstream instream(code);
 
   // parsing
-
+  jsil_parsert jsil_parser{message_handler};
   jsil_parser.clear();
   jsil_parser.set_file(irep_idt());
   jsil_parser.in=&instream;
-  jsil_parser.log.set_message_handler(message_handler);
-  jsil_scanner_init();
 
   bool result=jsil_parser.parse();
 
diff --git a/src/jsil/jsil_parser.cpp b/src/jsil/jsil_parser.cpp
index de11bc731e8..234f6510212 100644
--- a/src/jsil/jsil_parser.cpp
+++ b/src/jsil/jsil_parser.cpp
@@ -10,13 +10,3 @@ Author: Michael Tautschnig, tautschn@amazon.com
 /// Jsil Language
 
 #include "jsil_parser.h"
-
-jsil_parsert jsil_parser;
-
-extern char *yyjsiltext;
-
-int yyjsilerror(const std::string &error)
-{
-  jsil_parser.parse_error(error, yyjsiltext);
-  return 0;
-}
diff --git a/src/jsil/jsil_parser.h b/src/jsil/jsil_parser.h
index 2aad7767e34..c77e492259b 100644
--- a/src/jsil/jsil_parser.h
+++ b/src/jsil/jsil_parser.h
@@ -16,16 +16,24 @@ Author: Michael Tautschnig, tautschn@amazon.com
 
 #include "jsil_parse_tree.h"
 
-int yyjsilparse();
+class jsil_parsert;
+int yyjsilparse(jsil_parsert &);
+void jsil_scanner_init(jsil_parsert &);
 
 class jsil_parsert:public parsert
 {
 public:
+  explicit jsil_parsert(message_handlert &message_handler)
+    : parsert(message_handler)
+  {
+  }
+
   jsil_parse_treet parse_tree;
 
   virtual bool parse() override
   {
-    return yyjsilparse()!=0;
+    jsil_scanner_init(*this);
+    return yyjsilparse(*this) != 0;
   }
 
   virtual void clear() override
@@ -41,9 +49,4 @@ class jsil_parsert:public parsert
   std::string string_literal;
 };
 
-extern jsil_parsert jsil_parser;
-
-int yyjsilerror(const std::string &error);
-void jsil_scanner_init();
-
 #endif // CPROVER_JSIL_JSIL_PARSER_H
diff --git a/src/jsil/parser.y b/src/jsil/parser.y
index 7488353d034..31c96d972ed 100644
--- a/src/jsil/parser.y
+++ b/src/jsil/parser.y
@@ -1,13 +1,27 @@
 %{
 
 // #define YYDEBUG 1
-#define PARSER jsil_parser
+#define PARSER (*jsil_parser)
 
 #include "jsil_parser.h"
 
 int yyjsillex();
 extern char *yyjsiltext;
 
+static jsil_parsert *jsil_parser;
+int yyjsilparse(void);
+int yyjsilparse(jsil_parsert &_jsil_parser)
+{
+  jsil_parser = &_jsil_parser;
+  return yyjsilparse();
+}
+
+int yyjsilerror(const std::string &error)
+{
+  jsil_parser->parse_error(error, yyjsiltext);
+  return 0;
+}
+
 #define YYSTYPE unsigned
 #define YYSTYPE_IS_TRIVIAL 1
 
diff --git a/src/jsil/scanner.l b/src/jsil/scanner.l
index 1ed37abebfa..4ec6cef9336 100755
--- a/src/jsil/scanner.l
+++ b/src/jsil/scanner.l
@@ -17,13 +17,23 @@
 #include <ansi-c/literals/convert_float_literal.h>
 #include <ansi-c/literals/convert_string_literal.h>
 
-#define PARSER jsil_parser
+#define PARSER (*jsil_parser)
 #define YYSTYPE unsigned
 
 #include "jsil_parser.h"
 #include "jsil_y.tab.h"
 // extern int yyjsildebug;
 
+static jsil_parsert *jsil_parser;
+void jsil_scanner_init(jsil_parsert &_jsil_parser)
+{
+  jsil_parser = &_jsil_parser;
+  YY_FLUSH_BUFFER;
+  BEGIN(0);
+}
+
+int yyjsilerror(const std::string &error);
+
 #define loc() \
   { newstack(yyjsillval); PARSER.set_source_location(parser_stack(yyjsillval)); }
 
@@ -71,14 +81,6 @@ string_lit      ["]{s_char}*["]
 %x STRING_LITERAL_COMMENT
 %x STATEMENTS
 
-%{
-void jsil_scanner_init()
-{
-  // yyjsildebug=1;
-  YY_FLUSH_BUFFER;
-  BEGIN(0);
-}
-%}
  /* %option debug */
 
 %%

From 043b937213b75dc1e11d196d8fd10a9411bc3c6e Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 20 Dec 2023 13:24:14 +0000
Subject: [PATCH 06/16] json_parsert: construct with message handler

This both avoids an object of static lifetime as well as it fixes the
(transitive) use of the deprecated messaget() constructor.
---
 src/json/json_parser.cpp | 11 ++++++++---
 src/json/json_parser.h   | 15 +++++++--------
 src/json/parser.y        |  7 +++++--
 src/json/scanner.l       | 15 ++++++++++++++-
 4 files changed, 34 insertions(+), 14 deletions(-)

diff --git a/src/json/json_parser.cpp b/src/json/json_parser.cpp
index cb30114cb39..6576c61acdf 100644
--- a/src/json/json_parser.cpp
+++ b/src/json/json_parser.cpp
@@ -10,7 +10,12 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <fstream>
 
-json_parsert json_parser;
+int yyjsonparse(json_parsert &);
+
+bool json_parsert::parse()
+{
+  return yyjsonparse(*this) != 0;
+}
 
 // 'do it all' function
 bool parse_json(
@@ -19,10 +24,10 @@ bool parse_json(
   message_handlert &message_handler,
   jsont &dest)
 {
-  json_parser.clear();
+  json_parsert json_parser{message_handler};
+
   json_parser.set_file(filename);
   json_parser.in=&in;
-  json_parser.log.set_message_handler(message_handler);
 
   bool result=json_parser.parse();
 
diff --git a/src/json/json_parser.h b/src/json/json_parser.h
index 926a30e10bf..bbefec217f4 100644
--- a/src/json/json_parser.h
+++ b/src/json/json_parser.h
@@ -15,21 +15,22 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/parser.h>
 #include <util/json.h>
 
-int yyjsonparse();
 void yyjsonrestart(FILE *input_file);
 
 class json_parsert:public parsert
 {
 public:
+  explicit json_parsert(message_handlert &message_handler)
+    : parsert(message_handler)
+  {
+  }
+
   typedef std::stack<jsont, std::vector<jsont> > stackt;
   stackt stack;
 
   jsont &top() { return stack.top(); }
 
-  virtual bool parse() override
-  {
-    return yyjsonparse()!=0;
-  }
+  bool parse() override;
 
   void push(const jsont &x)
   {
@@ -50,9 +51,7 @@ class json_parsert:public parsert
   }
 };
 
-extern json_parsert json_parser;
-
-int yyjsonerror(const std::string &error);
+int yyjsonerror(json_parsert &, const std::string &error);
 
 // 'do it all' functions
 bool parse_json(
diff --git a/src/json/parser.y b/src/json/parser.y
index facaf48638d..1a787c4ce20 100644
--- a/src/json/parser.y
+++ b/src/json/parser.y
@@ -20,7 +20,7 @@
 
 #include <util/unicode.h>
 
-int yyjsonlex();
+int yyjsonlex(json_parsert &json_parser);
 extern char *yyjsontext;
 extern int yyjsonleng; // really an int, not a size_t
 
@@ -75,7 +75,7 @@ static std::string convert_TOK_NUMBER()
   return yyjsontext;
 }
 
-int yyjsonerror(const std::string &error)
+int yyjsonerror(json_parsert &json_parser, const std::string &error)
 {
   json_parser.parse_error(error, yyjsontext);
   return 0;
@@ -83,6 +83,9 @@ int yyjsonerror(const std::string &error)
 
 %}
 
+%parse-param {json_parsert &json_parser}
+%lex-param {json_parsert &json_parser}
+
 %token TOK_STRING
 %token TOK_NUMBER
 %token TOK_TRUE
diff --git a/src/json/scanner.l b/src/json/scanner.l
index c10efc414fb..027f8bc2bb9 100755
--- a/src/json/scanner.l
+++ b/src/json/scanner.l
@@ -24,7 +24,7 @@
 #pragma warning(disable:4005)
 #endif
 
-#define PARSER json_parser
+#define PARSER (*json_parser)
 
 #include "json_parser.h"
 #include "json_y.tab.h"
@@ -33,6 +33,19 @@
 #include <util/pragma_wnull_conversion.def> // IWYU pragma: keep
 #include <util/pragma_wdeprecated_register.def> // IWYU pragma: keep
 
+static json_parsert *json_parser;
+
+int yyjsonlex(void);
+
+int yyjsonlex(json_parsert &_json_parser)
+{
+  // our scanner is not reentrant
+  PRECONDITION(!json_parser);
+  json_parser = &_json_parser;
+  int result = yyjsonlex();
+  json_parser = nullptr;
+  return result;
+}
 %}
 
 string  \"\"|\"{chars}\"

From 462e66fb8469ad6645a7ffaa55077f5c9287755e Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 20 Dec 2023 13:24:39 +0000
Subject: [PATCH 07/16] statement_list_parsert: construct with message handler

This both avoids an object of static lifetime as well as it fixes the
(transitive) use of the deprecated messaget() constructor.
---
 src/statement-list/parser.y                    | 16 +++++++++++++++-
 src/statement-list/scanner.l                   |  6 ++++--
 src/statement-list/statement_list_language.cpp |  3 +--
 src/statement-list/statement_list_parser.cpp   | 13 ++-----------
 src/statement-list/statement_list_parser.h     | 14 +++++++++-----
 5 files changed, 31 insertions(+), 21 deletions(-)

diff --git a/src/statement-list/parser.y b/src/statement-list/parser.y
index 70b2ccce969..e7dcfb6d1e9 100644
--- a/src/statement-list/parser.y
+++ b/src/statement-list/parser.y
@@ -12,7 +12,7 @@
 #ifdef STATEMENT_LIST_DEBUG
 #define YYDEBUG 1
 #endif
-#define PARSER statement_list_parser
+#define PARSER (*statement_list_parser)
 
 #include "statement_list_parser.h"
 #include "converters/convert_string_value.h"
@@ -26,6 +26,20 @@
 int yystatement_listlex();
 extern char *yystatement_listtext;
 
+static statement_list_parsert *statement_list_parser;
+int yystatement_listparse(void);
+int yystatement_listparse(statement_list_parsert &_statement_list_parser)
+{
+  statement_list_parser = &_statement_list_parser;
+  return yystatement_listparse();
+}
+
+int yystatement_listerror(const std::string &error)
+{
+  statement_list_parser->parse_error(error, yystatement_listtext);
+  return 0;
+}
+
 #define YYSTYPE unsigned
 #define YYSTYPE_IS_TRIVIAL 1
 
diff --git a/src/statement-list/scanner.l b/src/statement-list/scanner.l
index a06e11cf1f6..e5b28692b75 100644
--- a/src/statement-list/scanner.l
+++ b/src/statement-list/scanner.l
@@ -41,7 +41,7 @@ static int isatty(int) { return 0; }
 #endif
 
 // Value inside of statement_list_parser.h.
-#define PARSER statement_list_parser
+#define PARSER (*statement_list_parser)
 
 // Sets the type of yystatement_listlval so that it can be used as the stack 
 // index.
@@ -62,11 +62,13 @@ static int isatty(int) { return 0; }
 #ifdef STATEMENT_LIST_DEBUG
 extern int yystatement_listdebug;
 #endif
-void statement_list_scanner_init()
+static statement_list_parsert *statement_list_parser;
+void statement_list_scanner_init(statement_list_parsert &_statement_list_parser)
 {
 #ifdef STATEMENT_LIST_DEBUG
   yystatement_listdebug=1;
 #endif
+  statement_list_parser = &_statement_list_parser;
   YY_FLUSH_BUFFER;
   BEGIN(0);
 }
diff --git a/src/statement-list/statement_list_language.cpp b/src/statement-list/statement_list_language.cpp
index bd5e28d185c..d1cc36b7b5b 100644
--- a/src/statement-list/statement_list_language.cpp
+++ b/src/statement-list/statement_list_language.cpp
@@ -60,12 +60,11 @@ bool statement_list_languaget::parse(
   const std::string &path,
   message_handlert &message_handler)
 {
-  statement_list_parser.clear();
+  statement_list_parsert statement_list_parser{message_handler};
   parse_path = path;
   statement_list_parser.set_line_no(0);
   statement_list_parser.set_file(path);
   statement_list_parser.in = &instream;
-  statement_list_scanner_init();
   bool result = statement_list_parser.parse();
 
   // store result
diff --git a/src/statement-list/statement_list_parser.cpp b/src/statement-list/statement_list_parser.cpp
index a5f10b1ff1e..6c5653cd6c6 100644
--- a/src/statement-list/statement_list_parser.cpp
+++ b/src/statement-list/statement_list_parser.cpp
@@ -21,10 +21,6 @@ Author: Matthias Weiss, matthias.weiss@diffblue.com
 #include <iostream>
 #include <iterator>
 
-statement_list_parsert statement_list_parser;
-
-extern char *yystatement_listtext;
-
 /// Searches for the name of the TIA module inside of its root
 /// expression.
 /// \param root: Expression that includes the element's name as a
@@ -337,13 +333,8 @@ void statement_list_parsert::add_function(const exprt &function)
 
 bool statement_list_parsert::parse()
 {
-  return yystatement_listparse() != 0;
-}
-
-int yystatement_listerror(const std::string &error)
-{
-  statement_list_parser.parse_error(error, yystatement_listtext);
-  return 0;
+  statement_list_scanner_init(*this);
+  return yystatement_listparse(*this) != 0;
 }
 
 void statement_list_parsert::clear()
diff --git a/src/statement-list/statement_list_parser.h b/src/statement-list/statement_list_parser.h
index 468e35ce05b..2031e132d82 100644
--- a/src/statement-list/statement_list_parser.h
+++ b/src/statement-list/statement_list_parser.h
@@ -16,9 +16,10 @@ Author: Matthias Weiss, matthias.weiss@diffblue.com
 
 #include "statement_list_parse_tree.h"
 
+class statement_list_parsert;
 /// Defined in statement_list_y.tab.cpp. Main function for the parse process
 /// generated by bison, performs all necessary steps to fill the parse tree.
-int yystatement_listparse();
+int yystatement_listparse(statement_list_parsert &);
 
 /// Responsible for starting the parse process and to translate the result into
 /// a statement_list_parse_treet. This parser works by using the expression
@@ -34,6 +35,12 @@ int yystatement_listparse();
 class statement_list_parsert : public parsert
 {
 public:
+  /// Constructor
+  explicit statement_list_parsert(message_handlert &message_handler)
+    : parsert(message_handler)
+  {
+  }
+
   /// Starts the parsing process and saves the result inside of this instance's
   /// parse tree.
   /// \return False if successful.
@@ -71,9 +78,6 @@ class statement_list_parsert : public parsert
   statement_list_parse_treet parse_tree;
 };
 
-/// Instance of the parser, used by other modules.
-extern statement_list_parsert statement_list_parser;
-
 /// Forwards any errors that are encountered during the parse process. This
 /// function gets called by the generated files of flex and bison.
 /// \param error: Error message.
@@ -82,6 +86,6 @@ int yystatement_listerror(const std::string &error);
 
 /// Defined in scanner.l. This function initialises the scanner by setting
 /// debug flags (if present) and its initial state.
-void statement_list_scanner_init();
+void statement_list_scanner_init(statement_list_parsert &);
 
 #endif // CPROVER_STATEMENT_LIST_STATEMENT_LIST_PARSER_H

From 2446e6dc4cbd62e837f42fe3ba96dffe2efec559 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 20 Dec 2023 13:25:06 +0000
Subject: [PATCH 08/16] assembler_parsert: construct with message handler

This both avoids an object of static lifetime as well as it fixes the
(transitive) use of the deprecated messaget() constructor.
---
 src/assembler/assembler_parser.cpp            |  6 ++--
 src/assembler/assembler_parser.h              | 14 ++++-----
 src/assembler/remove_asm.cpp                  | 30 +++++++++++++------
 src/assembler/remove_asm.h                    |  5 ++--
 src/assembler/scanner.l                       | 16 +++++++---
 src/cbmc/cbmc_parse_options.cpp               |  4 +--
 .../goto_analyzer_parse_options.cpp           |  4 +--
 src/goto-diff/goto_diff_parse_options.cpp     |  4 +--
 .../goto_instrument_parse_options.cpp         |  6 ++--
 src/goto-synthesizer/cegis_verifier.cpp       |  4 +--
 src/libcprover-cpp/api.cpp                    |  4 +--
 11 files changed, 58 insertions(+), 39 deletions(-)

diff --git a/src/assembler/assembler_parser.cpp b/src/assembler/assembler_parser.cpp
index 10200644d1d..0266de26ba9 100644
--- a/src/assembler/assembler_parser.cpp
+++ b/src/assembler/assembler_parser.cpp
@@ -8,11 +8,11 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "assembler_parser.h"
 
-assembler_parsert assembler_parser;
-
 extern char *yyassemblertext;
 
-int yyassemblererror(const std::string &error)
+int yyassemblererror(
+  assembler_parsert &assembler_parser,
+  const std::string &error)
 {
   assembler_parser.parse_error(error, yyassemblertext);
   return 0;
diff --git a/src/assembler/assembler_parser.h b/src/assembler/assembler_parser.h
index 76f03c71aaf..92d3a5d2023 100644
--- a/src/assembler/assembler_parser.h
+++ b/src/assembler/assembler_parser.h
@@ -14,9 +14,9 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <list>
 
-int yyassemblerlex();
-int yyassemblererror(const std::string &error);
-void assembler_scanner_init();
+class assembler_parsert;
+int yyassemblerlex(assembler_parsert &);
+int yyassemblererror(assembler_parsert &, const std::string &error);
 
 class assembler_parsert:public parsert
 {
@@ -37,13 +37,14 @@ class assembler_parsert:public parsert
     instructions.push_back(instructiont());
   }
 
-  assembler_parsert()
+  explicit assembler_parsert(message_handlert &message_handler)
+    : parsert(message_handler)
   {
   }
 
   virtual bool parse()
   {
-    yyassemblerlex();
+    yyassemblerlex(*this);
     return false;
   }
 
@@ -51,10 +52,7 @@ class assembler_parsert:public parsert
   {
     parsert::clear();
     instructions.clear();
-    // assembler_scanner_init();
   }
 };
 
-extern assembler_parsert assembler_parser;
-
 #endif // CPROVER_ASSEMBLER_ASSEMBLER_PARSER_H
diff --git a/src/assembler/remove_asm.cpp b/src/assembler/remove_asm.cpp
index 102c9524703..0979909f383 100644
--- a/src/assembler/remove_asm.cpp
+++ b/src/assembler/remove_asm.cpp
@@ -30,8 +30,13 @@ Date:   December 2014
 class remove_asmt
 {
 public:
-  remove_asmt(symbol_tablet &_symbol_table, goto_functionst &_goto_functions)
-    : symbol_table(_symbol_table), goto_functions(_goto_functions)
+  remove_asmt(
+    symbol_tablet &_symbol_table,
+    goto_functionst &_goto_functions,
+    message_handlert &message_handler)
+    : symbol_table(_symbol_table),
+      goto_functions(_goto_functions),
+      message_handler(message_handler)
   {
   }
 
@@ -44,6 +49,7 @@ class remove_asmt
 protected:
   symbol_tablet &symbol_table;
   goto_functionst &goto_functions;
+  message_handlert &message_handler;
 
   void process_function(const irep_idt &, goto_functionst::goto_functiont &);
 
@@ -228,7 +234,7 @@ void remove_asmt::process_instruction_gcc(
   const irep_idt &i_str = to_string_constant(code.asm_text()).value();
 
   std::istringstream str(id2string(i_str));
-  assembler_parser.clear();
+  assembler_parsert assembler_parser{message_handler};
   assembler_parser.in = &str;
   assembler_parser.parse();
 
@@ -399,7 +405,7 @@ void remove_asmt::process_instruction_msc(
   const irep_idt &i_str = to_string_constant(code.op0()).value();
 
   std::istringstream str(id2string(i_str));
-  assembler_parser.clear();
+  assembler_parsert assembler_parser{message_handler};
   assembler_parser.in = &str;
   assembler_parser.parse();
 
@@ -544,13 +550,17 @@ void remove_asmt::process_function(
     remove_skip(goto_function.body);
 }
 
-/// \copybrief remove_asm(goto_modelt &)
+/// \copybrief remove_asm(goto_modelt &, message_handlert &)
 ///
 /// \param goto_functions: The goto functions
 /// \param symbol_table: The symbol table
-void remove_asm(goto_functionst &goto_functions, symbol_tablet &symbol_table)
+/// \param message_handler: Message handler
+void remove_asm(
+  goto_functionst &goto_functions,
+  symbol_tablet &symbol_table,
+  message_handlert &message_handler)
 {
-  remove_asmt rem(symbol_table, goto_functions);
+  remove_asmt rem(symbol_table, goto_functions, message_handler);
   rem();
 }
 
@@ -561,9 +571,11 @@ void remove_asm(goto_functionst &goto_functions, symbol_tablet &symbol_table)
 /// Unrecognised assembly instructions are ignored.
 ///
 /// \param goto_model: The goto model
-void remove_asm(goto_modelt &goto_model)
+/// \param message_handler: Message handler
+void remove_asm(goto_modelt &goto_model, message_handlert &message_handler)
 {
-  remove_asm(goto_model.goto_functions, goto_model.symbol_table);
+  remove_asm(
+    goto_model.goto_functions, goto_model.symbol_table, message_handler);
 }
 
 bool has_asm(const goto_functionst &goto_functions)
diff --git a/src/assembler/remove_asm.h b/src/assembler/remove_asm.h
index 00b4346d285..e37ee640942 100644
--- a/src/assembler/remove_asm.h
+++ b/src/assembler/remove_asm.h
@@ -54,11 +54,12 @@ Date:   December 2014
 
 class goto_functionst;
 class goto_modelt;
+class message_handlert;
 class symbol_tablet;
 
-void remove_asm(goto_functionst &, symbol_tablet &);
+void remove_asm(goto_functionst &, symbol_tablet &, message_handlert &);
 
-void remove_asm(goto_modelt &);
+void remove_asm(goto_modelt &, message_handlert &);
 
 /// returns true iff the given goto functions use asm instructions
 bool has_asm(const goto_functionst &);
diff --git a/src/assembler/scanner.l b/src/assembler/scanner.l
index d975de73315..74930ea7aef 100755
--- a/src/assembler/scanner.l
+++ b/src/assembler/scanner.l
@@ -13,7 +13,7 @@
 #pragma warning(disable:4005)
 #endif
 
-#define PARSER assembler_parser
+#define PARSER (*assembler_parser)
 #define YYSTYPE unsigned
 #undef  ECHO
 #define ECHO
@@ -61,10 +61,18 @@ string_lit      ("L"|"u"|"U"|"u8")?["]{s_char}*["]
 %x LINE_COMMENT
 
 %{
-void assemlber_scanner_init()
+static assembler_parsert *assembler_parser;
+
+int yyassemblerlex(void);
+
+int yyassemblerlex(assembler_parsert &_assembler_parser)
 {
-  YY_FLUSH_BUFFER;
-  BEGIN(0);
+  // our scanner is not reentrant
+  PRECONDITION(!assembler_parser);
+  assembler_parser = &_assembler_parser;
+  int result = yyassemblerlex();
+  assembler_parser = nullptr;
+  return result;
 }
 %}
 
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index 5395a2eed4c..97a5d76c1d6 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -882,7 +882,7 @@ bool cbmc_parse_optionst::process_goto_program(
 {
   // Remove inline assembler; this needs to happen before
   // adding the library.
-  remove_asm(goto_model);
+  remove_asm(goto_model, log.get_message_handler());
 
   // add the library
   log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
@@ -894,7 +894,7 @@ bool cbmc_parse_optionst::process_goto_program(
   // library functions may introduce inline assembler
   while(has_asm(goto_model))
   {
-    remove_asm(goto_model);
+    remove_asm(goto_model, log.get_message_handler());
     link_to_library(
       goto_model, log.get_message_handler(), cprover_cpp_library_factory);
     link_to_library(
diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp
index f6463eca656..4c18f105002 100644
--- a/src/goto-analyzer/goto_analyzer_parse_options.cpp
+++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp
@@ -698,7 +698,7 @@ bool goto_analyzer_parse_optionst::process_goto_program(
 {
   // Remove inline assembler; this needs to happen before
   // adding the library.
-  remove_asm(goto_model);
+  remove_asm(goto_model, ui_message_handler);
 
   // add the library
   log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
@@ -708,7 +708,7 @@ bool goto_analyzer_parse_optionst::process_goto_program(
   // library functions may introduce inline assembler
   while(has_asm(goto_model))
   {
-    remove_asm(goto_model);
+    remove_asm(goto_model, ui_message_handler);
     link_to_library(
       goto_model, ui_message_handler, cprover_cpp_library_factory);
     link_to_library(goto_model, ui_message_handler, cprover_c_library_factory);
diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp
index 01068018927..97c98673100 100644
--- a/src/goto-diff/goto_diff_parse_options.cpp
+++ b/src/goto-diff/goto_diff_parse_options.cpp
@@ -176,7 +176,7 @@ bool goto_diff_parse_optionst::process_goto_program(
 {
   // Remove inline assembler; this needs to happen before
   // adding the library.
-  remove_asm(goto_model);
+  remove_asm(goto_model, ui_message_handler);
 
   // add the library
   log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
@@ -186,7 +186,7 @@ bool goto_diff_parse_optionst::process_goto_program(
   // library functions may introduce inline assembler
   while(has_asm(goto_model))
   {
-    remove_asm(goto_model);
+    remove_asm(goto_model, ui_message_handler);
     link_to_library(
       goto_model, ui_message_handler, cprover_cpp_library_factory);
     link_to_library(goto_model, ui_message_handler, cprover_c_library_factory);
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index cc78444fcd8..9957af70706 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -949,7 +949,7 @@ void goto_instrument_parse_optionst::do_indirect_call_and_rtti_removal(
   log.status() << "Virtual function removal" << messaget::eom;
   remove_virtual_functions(goto_model);
   log.status() << "Cleaning inline assembler statements" << messaget::eom;
-  remove_asm(goto_model);
+  remove_asm(goto_model, log.get_message_handler());
 }
 
 /// Remove function pointers that can be resolved by analysing const variables
@@ -1065,7 +1065,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
 
     // remove inline assembler as that may yield further library function calls
     // that need to be resolved
-    remove_asm(goto_model);
+    remove_asm(goto_model, ui_message_handler);
 
     // add the library
     log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
@@ -1076,7 +1076,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
     // library functions may introduce inline assembler
     while(has_asm(goto_model))
     {
-      remove_asm(goto_model);
+      remove_asm(goto_model, ui_message_handler);
       link_to_library(
         goto_model, ui_message_handler, cprover_cpp_library_factory);
       link_to_library(
diff --git a/src/goto-synthesizer/cegis_verifier.cpp b/src/goto-synthesizer/cegis_verifier.cpp
index 57bbfdf30fb..570fa2b9e0f 100644
--- a/src/goto-synthesizer/cegis_verifier.cpp
+++ b/src/goto-synthesizer/cegis_verifier.cpp
@@ -84,7 +84,7 @@ get_checked_pointer_from_null_pointer_check(const exprt &violation)
 void cegis_verifiert::preprocess_goto_model()
 {
   // Preprocess `goto_model`. Copied from `cbmc_parse_options.cpp`.
-  remove_asm(goto_model);
+  remove_asm(goto_model, log.get_message_handler());
   link_to_library(
     goto_model, log.get_message_handler(), cprover_cpp_library_factory);
   link_to_library(
@@ -92,7 +92,7 @@ void cegis_verifiert::preprocess_goto_model()
   // library functions may introduce inline assembler
   while(has_asm(goto_model))
   {
-    remove_asm(goto_model);
+    remove_asm(goto_model, log.get_message_handler());
     link_to_library(
       goto_model, log.get_message_handler(), cprover_cpp_library_factory);
     link_to_library(
diff --git a/src/libcprover-cpp/api.cpp b/src/libcprover-cpp/api.cpp
index 598da01eede..f2285331d22 100644
--- a/src/libcprover-cpp/api.cpp
+++ b/src/libcprover-cpp/api.cpp
@@ -178,7 +178,7 @@ bool api_sessiont::is_goto_binary(std::string &file) const
 bool api_sessiont::preprocess_model() const
 {
   // Remove inline assembler; this needs to happen before adding the library.
-  remove_asm(*implementation->model);
+  remove_asm(*implementation->model, *implementation->message_handler);
 
   // add the library
   messaget log{*implementation->message_handler};
@@ -191,7 +191,7 @@ bool api_sessiont::preprocess_model() const
   // library functions may introduce inline assembler
   while(has_asm(*implementation->model))
   {
-    remove_asm(*implementation->model);
+    remove_asm(*implementation->model, *implementation->message_handler);
     link_to_library(
       *implementation->model,
       *implementation->message_handler,

From 6ba69108d1881cf22ac1b75f975856e9ce487a46 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 20 Dec 2023 13:25:58 +0000
Subject: [PATCH 09/16] java_bytecode_parsert: construct with message handler

This both avoids an object of static lifetime as well as it fixes the
(transitive) use of the deprecated messaget() constructor.
---
 jbmc/src/java_bytecode/java_bytecode_parser.cpp | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/jbmc/src/java_bytecode/java_bytecode_parser.cpp b/jbmc/src/java_bytecode/java_bytecode_parser.cpp
index b7e02ddd859..ccf9375e717 100644
--- a/jbmc/src/java_bytecode/java_bytecode_parser.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_parser.cpp
@@ -27,8 +27,10 @@ Author: Daniel Kroening, kroening@kroening.com
 class java_bytecode_parsert final : public parsert
 {
 public:
-  explicit java_bytecode_parsert(bool skip_instructions)
-    : skip_instructions(skip_instructions)
+  java_bytecode_parsert(
+    bool skip_instructions,
+    message_handlert &message_handler)
+    : parsert(message_handler), skip_instructions(skip_instructions)
   {
   }
 
@@ -1809,9 +1811,9 @@ std::optional<java_bytecode_parse_treet> java_bytecode_parse(
   message_handlert &message_handler,
   bool skip_instructions)
 {
-  java_bytecode_parsert java_bytecode_parser(skip_instructions);
+  java_bytecode_parsert java_bytecode_parser(
+    skip_instructions, message_handler);
   java_bytecode_parser.in=&istream;
-  java_bytecode_parser.log.set_message_handler(message_handler);
 
   bool parser_result=java_bytecode_parser.parse();
 

From 3d6de5aaaf8239ecbe18172a0d6a8fd1fec3248d Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 20 Dec 2023 13:30:08 +0000
Subject: [PATCH 10/16] ansi_c_parsert: construct with message handler

This both avoids an object of static lifetime as well as it fixes the
(transitive) use of the deprecated messaget() constructor.
---
 src/ansi-c/ansi_c_language.cpp                | 12 ++++-----
 src/ansi-c/ansi_c_parser.cpp                  | 10 -------
 src/ansi-c/ansi_c_parser.h                    | 18 +++++++------
 src/ansi-c/builtin_factory.cpp                |  5 ++--
 src/ansi-c/parser.y                           | 16 +++++++++++-
 src/ansi-c/scanner.l                          | 26 ++++++++++---------
 .../contracts/contracts_wrangler.cpp          |  4 +--
 7 files changed, 48 insertions(+), 43 deletions(-)

diff --git a/src/ansi-c/ansi_c_language.cpp b/src/ansi-c/ansi_c_language.cpp
index c4eb9cadc14..0777f819673 100644
--- a/src/ansi-c/ansi_c_language.cpp
+++ b/src/ansi-c/ansi_c_language.cpp
@@ -71,17 +71,16 @@ bool ansi_c_languaget::parse(
   ansi_c_internal_additions(code, config.ansi_c.ts_18661_3_Floatn_types);
   std::istringstream codestr(code);
 
-  ansi_c_parser.clear();
+  ansi_c_parsert ansi_c_parser{message_handler};
   ansi_c_parser.set_file(ID_built_in);
   ansi_c_parser.in=&codestr;
-  ansi_c_parser.log.set_message_handler(message_handler);
   ansi_c_parser.for_has_scope=config.ansi_c.for_has_scope;
   ansi_c_parser.ts_18661_3_Floatn_types=config.ansi_c.ts_18661_3_Floatn_types;
   ansi_c_parser.cpp98=false; // it's not C++
   ansi_c_parser.cpp11=false; // it's not C++
   ansi_c_parser.mode=config.ansi_c.mode;
 
-  ansi_c_scanner_init();
+  ansi_c_scanner_init(ansi_c_parser);
 
   bool result=ansi_c_parser.parse();
 
@@ -90,7 +89,7 @@ bool ansi_c_languaget::parse(
     ansi_c_parser.set_line_no(0);
     ansi_c_parser.set_file(path);
     ansi_c_parser.in=&i_preprocessed;
-    ansi_c_scanner_init();
+    ansi_c_scanner_init(ansi_c_parser);
     result=ansi_c_parser.parse();
   }
 
@@ -197,13 +196,12 @@ bool ansi_c_languaget::to_expr(
 
   // parsing
 
-  ansi_c_parser.clear();
+  ansi_c_parsert ansi_c_parser{message_handler};
   ansi_c_parser.set_file(irep_idt());
   ansi_c_parser.in=&i_preprocessed;
-  ansi_c_parser.log.set_message_handler(message_handler);
   ansi_c_parser.mode=config.ansi_c.mode;
   ansi_c_parser.ts_18661_3_Floatn_types=config.ansi_c.ts_18661_3_Floatn_types;
-  ansi_c_scanner_init();
+  ansi_c_scanner_init(ansi_c_parser);
 
   bool result=ansi_c_parser.parse();
 
diff --git a/src/ansi-c/ansi_c_parser.cpp b/src/ansi-c/ansi_c_parser.cpp
index 9aa79de4ab4..c26911d93b0 100644
--- a/src/ansi-c/ansi_c_parser.cpp
+++ b/src/ansi-c/ansi_c_parser.cpp
@@ -10,8 +10,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "c_storage_spec.h"
 
-ansi_c_parsert ansi_c_parser;
-
 ansi_c_id_classt ansi_c_parsert::lookup(
   const irep_idt &base_name,
   irep_idt &identifier, // output
@@ -73,14 +71,6 @@ void ansi_c_parsert::add_tag_with_body(irept &tag)
   }
 }
 
-extern char *yyansi_ctext;
-
-int yyansi_cerror(const std::string &error)
-{
-  ansi_c_parser.parse_error(error, yyansi_ctext);
-  return 0;
-}
-
 void ansi_c_parsert::add_declarator(
   exprt &declaration,
   irept &declarator)
diff --git a/src/ansi-c/ansi_c_parser.h b/src/ansi-c/ansi_c_parser.h
index 4dde7752afe..060a684bf09 100644
--- a/src/ansi-c/ansi_c_parser.h
+++ b/src/ansi-c/ansi_c_parser.h
@@ -18,15 +18,17 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "ansi_c_parse_tree.h"
 #include "ansi_c_scope.h"
 
-int yyansi_cparse();
+class ansi_c_parsert;
+int yyansi_cparse(ansi_c_parsert &);
 
 class ansi_c_parsert:public parsert
 {
 public:
   ansi_c_parse_treet parse_tree;
 
-  ansi_c_parsert()
-    : tag_following(false),
+  explicit ansi_c_parsert(message_handlert &message_handler)
+    : parsert(message_handler),
+      tag_following(false),
       asm_block_following(false),
       parenthesis_counter(0),
       mode(modet::NONE),
@@ -35,11 +37,14 @@ class ansi_c_parsert:public parsert
       for_has_scope(false),
       ts_18661_3_Floatn_types(false)
   {
+    // set up global scope
+    scopes.clear();
+    scopes.push_back(scopet());
   }
 
   virtual bool parse() override
   {
-    return yyansi_cparse()!=0;
+    return yyansi_cparse(*this) != 0;
   }
 
   virtual void clear() override
@@ -166,9 +171,6 @@ class ansi_c_parsert:public parsert
   std::list<std::map<const irep_idt, bool>> pragma_cprover_stack;
 };
 
-extern ansi_c_parsert ansi_c_parser;
-
-int yyansi_cerror(const std::string &error);
-void ansi_c_scanner_init();
+void ansi_c_scanner_init(ansi_c_parsert &);
 
 #endif // CPROVER_ANSI_C_ANSI_C_PARSER_H
diff --git a/src/ansi-c/builtin_factory.cpp b/src/ansi-c/builtin_factory.cpp
index bfed926cb03..80cd8db2905 100644
--- a/src/ansi-c/builtin_factory.cpp
+++ b/src/ansi-c/builtin_factory.cpp
@@ -47,16 +47,15 @@ static bool convert(
 {
   std::istringstream in(s.str());
 
-  ansi_c_parser.clear();
+  ansi_c_parsert ansi_c_parser{message_handler};
   ansi_c_parser.set_file(ID_built_in);
   ansi_c_parser.in=&in;
-  ansi_c_parser.log.set_message_handler(message_handler);
   ansi_c_parser.for_has_scope=config.ansi_c.for_has_scope;
   ansi_c_parser.cpp98=false; // it's not C++
   ansi_c_parser.cpp11=false; // it's not C++
   ansi_c_parser.mode=config.ansi_c.mode;
 
-  ansi_c_scanner_init();
+  ansi_c_scanner_init(ansi_c_parser);
 
   if(ansi_c_parser.parse())
     return true;
diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y
index 5335593b46d..f2959d76171 100644
--- a/src/ansi-c/parser.y
+++ b/src/ansi-c/parser.y
@@ -13,13 +13,27 @@
 #ifdef ANSI_C_DEBUG
 #define YYDEBUG 1
 #endif
-#define PARSER ansi_c_parser
+#define PARSER (*ansi_c_parser)
 
 #include "ansi_c_parser.h"
 
 int yyansi_clex();
 extern char *yyansi_ctext;
 
+static ansi_c_parsert *ansi_c_parser;
+int yyansi_cparse(void);
+int yyansi_cparse(ansi_c_parsert &_ansi_c_parser)
+{
+  ansi_c_parser = &_ansi_c_parser;
+  return yyansi_cparse();
+}
+
+int yyansi_cerror(const std::string &error)
+{
+  ansi_c_parser->parse_error(error, yyansi_ctext);
+  return 0;
+}
+
 #include "parser_static.inc"
 
 #include "literals/convert_integer_literal.h"
diff --git a/src/ansi-c/scanner.l b/src/ansi-c/scanner.l
index a55fc3b1fc0..7794f34bd2e 100644
--- a/src/ansi-c/scanner.l
+++ b/src/ansi-c/scanner.l
@@ -38,7 +38,7 @@ static int isatty(int) { return 0; }
 #include "literals/convert_string_literal.h"
 #include "literals/unescape_string.h"
 
-#define PARSER ansi_c_parser
+#define PARSER (*ansi_c_parser)
 #define YYSTYPE unsigned
 #undef  ECHO
 #define ECHO
@@ -49,6 +49,19 @@ static int isatty(int) { return 0; }
 extern int yyansi_cdebug;
 #endif
 
+static ansi_c_parsert *ansi_c_parser;
+void ansi_c_scanner_init(ansi_c_parsert &_ansi_c_parser)
+{
+#ifdef ANSI_C_DEBUG
+  yyansi_cdebug=1;
+#endif
+  ansi_c_parser = &_ansi_c_parser;
+  YY_FLUSH_BUFFER;
+  BEGIN(0);
+}
+
+int yyansi_cerror(const std::string &error);
+
 #define loc() \
   { newstack(yyansi_clval); PARSER.set_source_location(parser_stack(yyansi_clval)); }
 
@@ -264,17 +277,6 @@ enable_or_disable ("enable"|"disable")
 %x CPROVER_PRAGMA
 %x OTHER_PRAGMA
 
-%{
-void ansi_c_scanner_init()
-{
-#ifdef ANSI_C_DEBUG
-  yyansi_cdebug=1;
-#endif
-  YY_FLUSH_BUFFER;
-  BEGIN(0);
-}
-%}
-
 %%
 
 <INITIAL>.|\n   { BEGIN(GRAMMAR);
diff --git a/src/goto-instrument/contracts/contracts_wrangler.cpp b/src/goto-instrument/contracts/contracts_wrangler.cpp
index b3aab30e54c..7c6dec33105 100644
--- a/src/goto-instrument/contracts/contracts_wrangler.cpp
+++ b/src/goto-instrument/contracts/contracts_wrangler.cpp
@@ -139,11 +139,11 @@ void contracts_wranglert::mangle(
 
   // Parse the fake function.
   std::istringstream is(pr.str());
-  ansi_c_parser.clear();
+  ansi_c_parsert ansi_c_parser{message_handler};
   ansi_c_parser.set_line_no(0);
   ansi_c_parser.set_file("<predicate>");
   ansi_c_parser.in = &is;
-  ansi_c_scanner_init();
+  ansi_c_scanner_init(ansi_c_parser);
   ansi_c_parser.parse();
 
   // Extract the invariants from prase_tree.

From 1ed367932ea2f16d4f5769f3d440a16a879be7ea Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 20 Dec 2023 13:35:29 +0000
Subject: [PATCH 11/16] cpp_parsert: construct with message handler

This both avoids an object of static lifetime as well as it fixes the
(transitive) use of the deprecated messaget() constructor.
---
 src/cpp/cpp_language.cpp     |  8 ++------
 src/cpp/cpp_parser.cpp       | 23 +++++------------------
 src/cpp/cpp_parser.h         | 12 ++++++------
 src/cpp/cpp_token_buffer.cpp |  2 --
 src/cpp/cpp_token_buffer.h   | 19 ++++++++++++++++---
 src/cpp/parse.cpp            | 19 +++++++++++--------
 6 files changed, 40 insertions(+), 43 deletions(-)

diff --git a/src/cpp/cpp_language.cpp b/src/cpp/cpp_language.cpp
index 7d6ae8351f3..b4bfd5e7dff 100644
--- a/src/cpp/cpp_language.cpp
+++ b/src/cpp/cpp_language.cpp
@@ -102,11 +102,9 @@ bool cpp_languaget::parse(
   std::istringstream i_preprocessed(o_preprocessed.str());
 
   // parsing
-
-  cpp_parser.clear();
+  cpp_parsert cpp_parser{message_handler};
   cpp_parser.set_file(path);
   cpp_parser.in=&i_preprocessed;
-  cpp_parser.log.set_message_handler(message_handler);
   cpp_parser.mode=config.ansi_c.mode;
 
   bool result=cpp_parser.parse();
@@ -245,11 +243,9 @@ bool cpp_languaget::to_expr(
   std::istringstream i_preprocessed(code);
 
   // parsing
-
-  cpp_parser.clear();
+  cpp_parsert cpp_parser{message_handler};
   cpp_parser.set_file(irep_idt());
   cpp_parser.in=&i_preprocessed;
-  cpp_parser.log.set_message_handler(message_handler);
 
   bool result=cpp_parser.parse();
 
diff --git a/src/cpp/cpp_parser.cpp b/src/cpp/cpp_parser.cpp
index 0d72414eec9..c4484638eb8 100644
--- a/src/cpp/cpp_parser.cpp
+++ b/src/cpp/cpp_parser.cpp
@@ -11,25 +11,12 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 
 #include "cpp_parser.h"
 
-#include <util/config.h>
-
-cpp_parsert cpp_parser;
-
-bool cpp_parse();
+bool cpp_parse(cpp_parsert &, message_handlert &);
 
 bool cpp_parsert::parse()
 {
-  // We use the ANSI-C scanner
-  ansi_c_parser.cpp98=true;
-  ansi_c_parser.cpp11 =
-    config.cpp.cpp_standard == configt::cppt::cpp_standardt::CPP11 ||
-    config.cpp.cpp_standard == configt::cppt::cpp_standardt::CPP14 ||
-    config.cpp.cpp_standard == configt::cppt::cpp_standardt::CPP17;
-  ansi_c_parser.ts_18661_3_Floatn_types=false;
-  ansi_c_parser.in=in;
-  ansi_c_parser.mode=mode;
-  ansi_c_parser.set_file(get_file());
-  ansi_c_parser.log.set_message_handler(log.get_message_handler());
-
-  return cpp_parse();
+  token_buffer.ansi_c_parser.in = in;
+  token_buffer.ansi_c_parser.mode = mode;
+  token_buffer.ansi_c_parser.set_file(get_file());
+  return cpp_parse(*this, log.get_message_handler());
 }
diff --git a/src/cpp/cpp_parser.h b/src/cpp/cpp_parser.h
index 1813872bf76..6029fca6ea2 100644
--- a/src/cpp/cpp_parser.h
+++ b/src/cpp/cpp_parser.h
@@ -34,10 +34,12 @@ class cpp_parsert:public parsert
     asm_block_following=false;
   }
 
-  cpp_parsert():
-    mode(configt::ansi_ct::flavourt::ANSI),
-    recognize_wchar_t(true),
-    asm_block_following(false)
+  explicit cpp_parsert(message_handlert &message_handler)
+    : parsert(message_handler),
+      mode(configt::ansi_ct::flavourt::ANSI),
+      recognize_wchar_t(true),
+      token_buffer(message_handler),
+      asm_block_following(false)
   {
   }
 
@@ -67,6 +69,4 @@ class cpp_parsert:public parsert
   bool asm_block_following;
 };
 
-extern cpp_parsert cpp_parser;
-
 #endif // CPROVER_CPP_CPP_PARSER_H
diff --git a/src/cpp/cpp_token_buffer.cpp b/src/cpp/cpp_token_buffer.cpp
index df7e918f8a7..85a1a56d5bc 100644
--- a/src/cpp/cpp_token_buffer.cpp
+++ b/src/cpp/cpp_token_buffer.cpp
@@ -11,8 +11,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 
 #include "cpp_token_buffer.h"
 
-#include <ansi-c/ansi_c_parser.h>
-
 int cpp_token_buffert::LookAhead(unsigned offset)
 {
   PRECONDITION(current_pos <= token_vector.size());
diff --git a/src/cpp/cpp_token_buffer.h b/src/cpp/cpp_token_buffer.h
index 4d3acdbfc3c..d9b5f20139c 100644
--- a/src/cpp/cpp_token_buffer.h
+++ b/src/cpp/cpp_token_buffer.h
@@ -12,17 +12,28 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #ifndef CPROVER_CPP_CPP_TOKEN_BUFFER_H
 #define CPROVER_CPP_CPP_TOKEN_BUFFER_H
 
+#include <util/config.h>
+#include <util/invariant.h>
+
+#include <ansi-c/ansi_c_parser.h>
+
 #include "cpp_token.h"
 
 #include <list>
 
-#include <util/invariant.h>
-
 class cpp_token_buffert
 {
 public:
-  cpp_token_buffert():current_pos(0)
+  explicit cpp_token_buffert(message_handlert &message_handler)
+    : ansi_c_parser(message_handler), current_pos(0)
   {
+    // We use the ANSI-C scanner
+    ansi_c_parser.cpp98 = true;
+    ansi_c_parser.cpp11 =
+      config.cpp.cpp_standard == configt::cppt::cpp_standardt::CPP11 ||
+      config.cpp.cpp_standard == configt::cppt::cpp_standardt::CPP14 ||
+      config.cpp.cpp_standard == configt::cppt::cpp_standardt::CPP17;
+    ansi_c_parser.ts_18661_3_Floatn_types = false;
   }
 
   typedef unsigned int post;
@@ -51,6 +62,8 @@ class cpp_token_buffert
     return tokens.back();
   }
 
+  ansi_c_parsert ansi_c_parser;
+
 protected:
   typedef std::list<cpp_tokent> tokenst;
   tokenst tokens;
diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp
index a0ce60aca87..910d91a5811 100644
--- a/src/cpp/parse.cpp
+++ b/src/cpp/parse.cpp
@@ -195,9 +195,10 @@ void new_scopet::print_rec(std::ostream &out, unsigned indent) const
 class Parser // NOLINT(readability/identifiers)
 {
 public:
-  explicit Parser(cpp_parsert &_cpp_parser)
+  Parser(cpp_parsert &_cpp_parser, message_handlert &message_handler)
     : lex(_cpp_parser.token_buffer),
-      parser(_cpp_parser),
+      parse_tree(_cpp_parser.parse_tree),
+      message_handler(message_handler),
       max_errors(10),
       cpp11(
         config.cpp.cpp_standard == configt::cppt::cpp_standardt::CPP11 ||
@@ -212,7 +213,8 @@ class Parser // NOLINT(readability/identifiers)
 
 protected:
   cpp_token_buffert &lex;
-  cpp_parsert &parser;
+  cpp_parse_treet &parse_tree;
+  message_handlert &message_handler;
 
   // scopes
   new_scopet root_scope;
@@ -517,8 +519,9 @@ bool Parser::SyntaxError()
 
     message+="'";
 
-    parser.log.error().source_location = source_location;
-    parser.log.error() << message << messaget::eom;
+    messaget log{message_handler};
+    log.error().source_location = source_location;
+    log.error() << message << messaget::eom;
   }
 
   return ++number_of_errors < max_errors;
@@ -8381,7 +8384,7 @@ bool Parser::operator()()
 
   while(rProgram(item))
   {
-    parser.parse_tree.items.push_back(item);
+    parse_tree.items.push_back(item);
     item.clear();
   }
 
@@ -8392,8 +8395,8 @@ bool Parser::operator()()
   return number_of_errors!=0;
 }
 
-bool cpp_parse()
+bool cpp_parse(cpp_parsert &cpp_parser, message_handlert &message_handler)
 {
-  Parser parser(cpp_parser);
+  Parser parser(cpp_parser, message_handler);
   return parser();
 }

From fc7b43e04d871ac2cd1e4c70a63a6bcfecadcead Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 20 Dec 2023 13:22:14 +0000
Subject: [PATCH 12/16] 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 | 8 --------
 src/util/parser.h  | 8 +-------
 2 files changed, 1 insertion(+), 15 deletions(-)

diff --git a/src/util/message.h b/src/util/message.h
index 23476ce4e9c..431f27a6ca6 100644
--- a/src/util/message.h
+++ b/src/util/message.h
@@ -15,7 +15,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <sstream>
 #include <string>
 
-#include "deprecate.h"
 #include "invariant.h"
 #include "source_location.h"
 
@@ -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 c19aeb58977..b134df85cf4 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"
 
@@ -40,8 +39,6 @@ class parsert
     last_line.clear();
   }
 
-  DEPRECATED(SINCE(2023, 12, 20, "use parsert(message_handler) instead"))
-  parsert():in(nullptr) { clear(); }
   explicit parsert(message_handlert &message_handler)
     : in(nullptr), log(message_handler)
   {
@@ -138,11 +135,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;

From 458535ebe9f6b73a61148d42a134624533ffc959 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Mon, 14 Jan 2019 17:22:14 +0000
Subject: [PATCH 13/16] Remove -Wno-deprecated-declarations from compiler
 options

All uses of deprecated functions have been replaced.
---
 CMakeLists.txt | 4 ++--
 src/config.inc | 1 -
 2 files changed, 2 insertions(+), 3 deletions(-)

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 540f840f247..56aa7f6807b 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -78,7 +78,7 @@ if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "GNU")
     #   Enable lots of warnings
     set(CMAKE_CXX_FLAGS
         "${CMAKE_CXX_FLAGS} -Wall -Wpedantic -Werror -Wswitch-enum \
-         -Wno-deprecated-declarations -Wno-maybe-uninitialized")
+         -Wno-maybe-uninitialized")
 elseif("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR
        "${CMAKE_CXX_COMPILER_ID}" STREQUAL "AppleClang")
     #   Ensure NDEBUG is not set for release builds
@@ -86,7 +86,7 @@ elseif("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR
     set(CMAKE_CXX_FLAGS_RELWITHDEBINFO "-O2 -g")
     #   Enable lots of warnings
     set(CMAKE_CXX_FLAGS
-        "${CMAKE_CXX_FLAGS} -Wall -Wpedantic -Werror -Wswitch-enum -Wno-deprecated-declarations")
+        "${CMAKE_CXX_FLAGS} -Wall -Wpedantic -Werror -Wswitch-enum")
 elseif("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
     # This would be the place to enable warnings for Windows builds, although
     # config.inc doesn't seem to do that currently
diff --git a/src/config.inc b/src/config.inc
index 2f41286fb9e..6ce2bf88e91 100644
--- a/src/config.inc
+++ b/src/config.inc
@@ -6,7 +6,6 @@ ifeq ($(BUILD_ENV),MSVC)
   #CXXFLAGS += /Wall /WX
 else
   CXXFLAGS += -Wall -pedantic -Werror -Wswitch-enum
-  CXXFLAGS += -Wno-deprecated-declarations
   # GCC only, silence clang warning
   CXXFLAGS += -Wno-maybe-uninitialized -Wno-unknown-warning-option
 endif

From db11df7c266a34ee8f4e10db6d016c761e903fd9 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 12 Dec 2023 17:49:44 +0000
Subject: [PATCH 14/16] WIP: String solver deprecation cleanup

---
 .../strings/string_constraint_generator.h     |  4 +-
 .../string_constraint_generator_valueof.cpp   | 80 +------------------
 2 files changed, 3 insertions(+), 81 deletions(-)

diff --git a/src/solvers/strings/string_constraint_generator.h b/src/solvers/strings/string_constraint_generator.h
index f439e5f28b3..2d1705bf25a 100644
--- a/src/solvers/strings/string_constraint_generator.h
+++ b/src/solvers/strings/string_constraint_generator.h
@@ -273,7 +273,7 @@ class string_constraint_generatort final
   /// \todo This function is underspecified, we do not compute the exact value
   /// but over approximate it.
   /// \deprecated This is Java specific and should be implemented in Java.
-  DEPRECATED(SINCE(2017, 10, 5, "Java specific, should be implemented in Java"))
+  // DEPRECATED(SINCE(2017, 10, 5, "Java specific, should be implemented in Java"))
   std::pair<exprt, string_constraintst>
   add_axioms_for_code_point_count(const function_application_exprt &f);
 
@@ -283,7 +283,7 @@ class string_constraint_generatort final
   /// argument code points and we approximate this by saying the result is
   /// between index + offset and index + 2 * offset.
   /// \deprecated This is Java specific and should be implemented in Java.
-  DEPRECATED(SINCE(2017, 10, 5, "Java specific, should be implemented in Java"))
+  // DEPRECATED(SINCE(2017, 10, 5, "Java specific, should be implemented in Java"))
   std::pair<exprt, string_constraintst>
   add_axioms_for_offset_by_code_point(const function_application_exprt &f);
 
diff --git a/src/solvers/strings/string_constraint_generator_valueof.cpp b/src/solvers/strings/string_constraint_generator_valueof.cpp
index 039557734a1..34249af6e79 100644
--- a/src/solvers/strings/string_constraint_generator_valueof.cpp
+++ b/src/solvers/strings/string_constraint_generator_valueof.cpp
@@ -174,84 +174,6 @@ string_constraint_generatort::add_axioms_for_string_of_int_with_radix(
   return {from_integer(0, get_return_code_type()), std::move(result2)};
 }
 
-/// Returns the integer value represented by the character.
-/// \param chr: a character expression in the following set:
-///   0123456789abcdef
-/// \return an integer expression
-static exprt int_of_hex_char(const exprt &chr)
-{
-  const exprt zero_char = from_integer('0', chr.type());
-  const exprt nine_char = from_integer('9', chr.type());
-  const exprt a_char = from_integer('a', chr.type());
-  return if_exprt(
-    binary_relation_exprt(chr, ID_gt, nine_char),
-    plus_exprt(from_integer(10, chr.type()), minus_exprt(chr, a_char)),
-    minus_exprt(chr, zero_char));
-}
-
-/// Add axioms stating that the string `res` corresponds to the integer
-/// argument written in hexadecimal.
-/// \deprecated use add_axioms_from_int_with_radix instead
-/// \param res: string expression for the result
-/// \param i: an integer argument
-/// \return code 0 on success
-DEPRECATED(SINCE(2017, 10, 5, "use add_axioms_for_string_of_int_with_radix"))
-std::pair<exprt, string_constraintst>
-string_constraint_generatort::add_axioms_from_int_hex(
-  const array_string_exprt &res,
-  const exprt &i)
-{
-  const typet &type = i.type();
-  PRECONDITION(type.id() == ID_signedbv);
-  string_constraintst constraints;
-  const typet &index_type = res.length_type();
-  const typet &char_type = to_type_with_subtype(res.content().type()).subtype();
-  exprt sixteen = from_integer(16, index_type);
-  exprt minus_char = from_integer('-', char_type);
-  exprt zero_char = from_integer('0', char_type);
-  exprt nine_char = from_integer('9', char_type);
-  exprt a_char = from_integer('a', char_type);
-  exprt f_char = from_integer('f', char_type);
-
-  size_t max_size = 8;
-  constraints.existential.push_back(and_exprt(
-    greater_than(array_pool.get_or_create_length(res), 0),
-    less_than_or_equal_to(array_pool.get_or_create_length(res), max_size)));
-
-  for(size_t size = 1; size <= max_size; size++)
-  {
-    exprt sum = from_integer(0, type);
-    exprt all_numbers = true_exprt();
-    exprt chr = res[0];
-
-    for(size_t j = 0; j < size; j++)
-    {
-      chr = res[j];
-      exprt chr_int = int_of_hex_char(chr);
-      sum = plus_exprt(mult_exprt(sum, sixteen), typecast_exprt(chr_int, type));
-      or_exprt is_number(
-        and_exprt(
-          binary_relation_exprt(chr, ID_ge, zero_char),
-          binary_relation_exprt(chr, ID_le, nine_char)),
-        and_exprt(
-          binary_relation_exprt(chr, ID_ge, a_char),
-          binary_relation_exprt(chr, ID_le, f_char)));
-      all_numbers = and_exprt(all_numbers, is_number);
-    }
-
-    const equal_exprt premise =
-      equal_to(array_pool.get_or_create_length(res), size);
-    constraints.existential.push_back(
-      implies_exprt(premise, and_exprt(equal_exprt(i, sum), all_numbers)));
-
-    // disallow 0s at the beginning
-    if(size > 1)
-      constraints.existential.push_back(
-        implies_exprt(premise, not_exprt(equal_exprt(res[0], zero_char))));
-  }
-  return {from_integer(0, get_return_code_type()), std::move(constraints)};
-}
-
 /// Add axioms corresponding to the Integer.toHexString(I) java function
 /// \param f: function application with an integer argument
 /// \return code 0 on success
@@ -262,7 +184,7 @@ string_constraint_generatort::add_axioms_from_int_hex(
   PRECONDITION(f.arguments().size() == 3);
   const array_string_exprt res =
     array_pool.find(f.arguments()[1], f.arguments()[0]);
-  return add_axioms_from_int_hex(res, f.arguments()[2]);
+  return add_axioms_for_string_of_int_with_radix(res, f.arguments()[2], from_integer(16, unsignedbv_typet{8}) , 0);
 }
 
 /// Add axioms making the return value true if the given string is a correct

From 8a27a9226c8763432a26b48b254ca5752cacd2c4 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 12 Dec 2023 17:49:57 +0000
Subject: [PATCH 15/16] De-deprecated source_locationt methods

---
 src/util/source_location.h | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/util/source_location.h b/src/util/source_location.h
index fe99c578fb3..aabdeb911eb 100644
--- a/src/util/source_location.h
+++ b/src/util/source_location.h
@@ -60,7 +60,7 @@ class source_locationt:public irept
   //    to adjust all source locations.
   // 3) The name of the function is not strictly a source location.
   // It will be removed.
-  DEPRECATED(SINCE(2022, 10, 13, "use identifier of containing function"))
+  // DEPRECATED(SINCE(2022, 10, 13, "use identifier of containing function"))
   const irep_idt &get_function() const
   {
     return get(ID_function);
@@ -126,7 +126,7 @@ class source_locationt:public irept
     set(ID_column, column);
   }
 
-  DEPRECATED(SINCE(2022, 10, 13, "use identifier of containing function"))
+  // DEPRECATED(SINCE(2022, 10, 13, "use identifier of containing function"))
   void set_function(const irep_idt &function)
   {
     set(ID_function, function);

From e23573d5111c18537338f21fcee50bc03f04804d Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 12 Dec 2023 19:57:34 +0000
Subject: [PATCH 16/16] WIP, create PRs

---
 src/analyses/ai.h         | 4 ++--
 src/analyses/ai_storage.h | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/analyses/ai.h b/src/analyses/ai.h
index a4f0bc34e69..df5d5a4caeb 100644
--- a/src/analyses/ai.h
+++ b/src/analyses/ai.h
@@ -589,7 +589,7 @@ class ait : public ai_recursive_interproceduralt
   // Not recommended as it will throw an exception if a location has not
   // been reached in an analysis and there is no (other) way of telling
   // if a location has been reached.
-  DEPRECATED(SINCE(2019, 08, 01, "use abstract_state_{before,after} instead"))
+  // DEPRECATED(SINCE(2019, 08, 01, "use abstract_state_{before,after} instead"))
   const domainT &operator[](locationt l) const
   {
     auto p = storage->abstract_state_before(l, *domain_factory);
@@ -607,7 +607,7 @@ class ait : public ai_recursive_interproceduralt
   // Support the legacy get_state interface which is needed for a few domains
   // This is one of the few users of the legacy get_state(locationt) method
   // in location_sensitive_storaget.
-  DEPRECATED(SINCE(2019, 08, 01, "use get_state(trace_ptrt p) instead"))
+  // DEPRECATED(SINCE(2019, 08, 01, "use get_state(trace_ptrt p) instead"))
   virtual statet &get_state(locationt l)
   {
     auto &s = dynamic_cast<location_sensitive_storaget &>(*storage);
diff --git a/src/analyses/ai_storage.h b/src/analyses/ai_storage.h
index 6811f4ded2f..f09bb3c8b93 100644
--- a/src/analyses/ai_storage.h
+++ b/src/analyses/ai_storage.h
@@ -200,7 +200,7 @@ class location_sensitive_storaget : public trace_map_storaget
   // Care should be exercised in using this.  It is possible to create domains
   // without any corresponding history object(s).  This can lead to somewhat
   // unexpected behaviour depending on which APIs you use.
-  DEPRECATED(SINCE(2019, 08, 01, "use get_state(trace_ptrt p) instead"))
+  // DEPRECATED(SINCE(2019, 08, 01, "use get_state(trace_ptrt p) instead"))
   statet &get_state(locationt l, const ai_domain_factory_baset &fac)
   {
     typename state_mapt::const_iterator it = state_map.find(l);