Skip to content

Commit

Permalink
Merge pull request #8245 from tautschnig/no-reentrant-c-scanner
Browse files Browse the repository at this point in the history
C/C++ front-end: Revert scanner re-entrancy
  • Loading branch information
kroening authored Mar 18, 2024
2 parents 1fd7011 + 08d6d67 commit c7d8e2e
Show file tree
Hide file tree
Showing 10 changed files with 661 additions and 702 deletions.
4 changes: 4 additions & 0 deletions src/ansi-c/ansi_c_language.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -82,13 +82,16 @@ bool ansi_c_languaget::parse(
ansi_c_parser.cpp11=false; // it's not C++
ansi_c_parser.mode=config.ansi_c.mode;

ansi_c_scanner_init(ansi_c_parser);

bool result=ansi_c_parser.parse();

if(!result)
{
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_parser);
result=ansi_c_parser.parse();
}

Expand Down Expand Up @@ -202,6 +205,7 @@ bool ansi_c_languaget::to_expr(
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_parser);

bool result=ansi_c_parser.parse();

Expand Down
17 changes: 0 additions & 17 deletions src/ansi-c/ansi_c_parser.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -10,23 +10,6 @@ Author: Daniel Kroening, [email protected]

#include "c_storage_spec.h"

int yyansi_clex_init_extra(ansi_c_parsert *, void **);
int yyansi_clex_destroy(void *);
int yyansi_cparse(ansi_c_parsert &, void *);
void yyansi_cset_debug(int, void *);

bool ansi_c_parsert::parse()
{
void *scanner;
yyansi_clex_init_extra(this, &scanner);
#ifdef ANSI_C_DEBUG
yyansi_cset_debug(1, scanner);
#endif
bool parse_fail = yyansi_cparse(*this, scanner) != 0;
yyansi_clex_destroy(scanner);
return parse_fail;
}

ansi_c_id_classt ansi_c_parsert::lookup(
const irep_idt &base_name,
irep_idt &identifier, // output
Expand Down
10 changes: 9 additions & 1 deletion src/ansi-c/ansi_c_parser.h
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,9 @@ Author: Daniel Kroening, [email protected]
#include "ansi_c_parse_tree.h"
#include "ansi_c_scope.h"

class ansi_c_parsert;
int yyansi_cparse(ansi_c_parsert &);

class ansi_c_parsert:public parsert
{
public:
Expand All @@ -41,7 +44,10 @@ class ansi_c_parsert:public parsert
scopes.push_back(scopet());
}

bool parse() override;
bool parse() override
{
return yyansi_cparse(*this) != 0;
}

void clear() override
{
Expand Down Expand Up @@ -169,4 +175,6 @@ class ansi_c_parsert:public parsert
std::list<std::map<const irep_idt, bool>> pragma_cprover_stack;
};

void ansi_c_scanner_init(ansi_c_parsert &);

#endif // CPROVER_ANSI_C_ANSI_C_PARSER_H
2 changes: 2 additions & 0 deletions src/ansi-c/builtin_factory.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -58,6 +58,8 @@ static bool convert(
ansi_c_parser.cpp11=false; // it's not C++
ansi_c_parser.mode=config.ansi_c.mode;

ansi_c_scanner_init(ansi_c_parser);

if(ansi_c_parser.parse())
return true;

Expand Down
Loading

0 comments on commit c7d8e2e

Please sign in to comment.