Skip to content

Commit

Permalink
JSIL front-end: no need for parser reentrancy
Browse files Browse the repository at this point in the history
Just make sure it isn't used in a reentrant manner.
  • Loading branch information
tautschnig committed Jan 11, 2024
1 parent 69bb2b6 commit 6682802
Show file tree
Hide file tree
Showing 2 changed files with 17 additions and 2 deletions.
2 changes: 2 additions & 0 deletions src/jsil/jsil_parser.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -10,3 +10,5 @@ Author: Michael Tautschnig, [email protected]
/// Jsil Language

#include "jsil_parser.h"

int jsil_parsert::instance_count = 0;
17 changes: 15 additions & 2 deletions src/jsil/jsil_parser.h
Original file line number Diff line number Diff line change
Expand Up @@ -26,17 +26,27 @@ class jsil_parsert:public parsert
explicit jsil_parsert(message_handlert &message_handler)
: parsert(message_handler)
{
// Simplistic check that we don't attempt to do reentrant parsing as the
// Bison-generated parser has global state.
PRECONDITION(++instance_count == 1);
}

Check warning on line 32 in src/jsil/jsil_parser.h

View check run for this annotation

Codecov / codecov/patch

src/jsil/jsil_parser.h#L31-L32

Added lines #L31 - L32 were not covered by tests

jsil_parsert(const jsil_parsert &) = delete;

~jsil_parsert() override
{
--instance_count;

Check warning on line 38 in src/jsil/jsil_parser.h

View check run for this annotation

Codecov / codecov/patch

src/jsil/jsil_parser.h#L36-L38

Added lines #L36 - L38 were not covered by tests
}

jsil_parse_treet parse_tree;

virtual bool parse() override
bool parse() override

Check warning on line 43 in src/jsil/jsil_parser.h

View check run for this annotation

Codecov / codecov/patch

src/jsil/jsil_parser.h#L43

Added line #L43 was not covered by tests
{
jsil_scanner_init(*this);
return yyjsilparse(*this) != 0;
}

virtual void clear() override
void clear() override

Check warning on line 49 in src/jsil/jsil_parser.h

View check run for this annotation

Codecov / codecov/patch

src/jsil/jsil_parser.h#L49

Added line #L49 was not covered by tests
{
parsert::clear();
parse_tree.clear();
Expand All @@ -47,6 +57,9 @@ class jsil_parsert:public parsert

// internal state of the scanner
std::string string_literal;

protected:
static int instance_count;
};

#endif // CPROVER_JSIL_JSIL_PARSER_H

0 comments on commit 6682802

Please sign in to comment.