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 #include -#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 */ %% 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