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.

Author: tautschnig

Diff for: src/ansi-c/ansi_c_language.cpp

@@ -71,17 +71,16 @@ bool ansi_c_languaget::parse(
   ansi_c_internal_additions(code);
   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 for: src/ansi-c/ansi_c_parser.cpp

@@ -10,8 +10,6 @@ Author: Daniel Kroening, [email protected]
 
 #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 for: src/ansi-c/ansi_c_parser.h

@@ -18,15 +18,17 @@ Author: Daniel Kroening, [email protected]
 #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 for: 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=∈
-  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 for: 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 for: 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 for: 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.