Skip to content

Commit 95ec97e

Browse files
committed
JSIL front-end: no need for parser reentrancy
Just make sure it isn't used in a reentrant manner.
1 parent ede5ea4 commit 95ec97e

File tree

4 files changed

+119
-117
lines changed

4 files changed

+119
-117
lines changed

src/jsil/jsil_parser.cpp

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,8 @@ Author: Michael Tautschnig, [email protected]
1111

1212
#include "jsil_parser.h"
1313

14+
int jsil_parsert::instance_count = 0;
15+
1416
int yyjsillex_init_extra(jsil_parsert *, void **);
1517
int yyjsillex_destroy(void *);
1618
int yyjsilparse(jsil_parsert &, void *);

src/jsil/jsil_parser.h

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,15 @@ class jsil_parsert:public parsert
2222
explicit jsil_parsert(message_handlert &message_handler)
2323
: parsert(message_handler)
2424
{
25+
// simplistic check that we don't attempt to do reentrant parsing
26+
PRECONDITION(++instance_count == 1);
27+
}
28+
29+
jsil_parsert(const jsil_parsert &) = delete;
30+
31+
~jsil_parsert() override
32+
{
33+
--instance_count;
2534
}
2635

2736
jsil_parse_treet parse_tree;
@@ -39,6 +48,9 @@ class jsil_parsert:public parsert
3948

4049
// internal state of the scanner
4150
std::string string_literal;
51+
52+
protected:
53+
static int instance_count;
4254
};
4355

4456
#endif // CPROVER_JSIL_JSIL_PARSER_H

src/jsil/parser.y

Lines changed: 1 addition & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@
55

66
#include "jsil_parser.h"
77

8-
int yyjsillex(unsigned *, void *);
8+
int yyjsillex(void *);
99
char *yyjsilget_text(void *);
1010

1111
int yyjsilerror(
@@ -38,18 +38,8 @@ int yyjsilerror(
3838
// unreachable code
3939
#pragma warning(disable:4702)
4040
#endif
41-
42-
// yynerrs may never be used. Will be fixed when bison > 3.8.2 is released (see
43-
// http://git.savannah.gnu.org/cgit/bison.git/commit/?id=a166d5450e3f47587b98f6005f9f5627dbe21a5b)
44-
#ifdef __clang__
45-
# pragma clang diagnostic ignored "-Wunused-but-set-variable"
46-
#endif
4741
%}
4842

49-
// Should be "%define api.pure full" instead of "%pure-parser", but macOS ships
50-
// bison 2.3, which doesn't yet support this. We have to invoke bison with
51-
// -Wno-deprecated on all platforms other than macOS.
52-
%pure-parser
5343
%parse-param {jsil_parsert &jsil_parser}
5444
%parse-param {void *scanner}
5545
%lex-param {void *scanner}

0 commit comments

Comments
 (0)