diff --git a/src/ansi-c/ansi_c_language.cpp b/src/ansi-c/ansi_c_language.cpp index af29ed2599e6..b2aa7621382e 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); 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 9aa79de4ab4f..c26911d93b0a 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 4dde7752afec..060a684bf098 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> 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 0d9de3c48cd5..6375a3c73638 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=∈ - 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 5335593b46d2..f2959d76171f 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 a55fc3b1fc0b..7794f34bd2e0 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); -} -%} - %% .|\n { BEGIN(GRAMMAR); diff --git a/src/goto-instrument/contracts/contracts_wrangler.cpp b/src/goto-instrument/contracts/contracts_wrangler.cpp index b3aab30e54c2..7c6dec331059 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(""); 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.