Skip to content

Commit 08d6d67

Browse files
committed
C/C++ front-end: Revert scanner re-entrancy
There is no need for scanner re-entrancy, and using flex' re-entrancy options fails the build on some macOS configurations. Partly reverts 1f240bc.
1 parent 1fd7011 commit 08d6d67

10 files changed

+661
-702
lines changed

src/ansi-c/ansi_c_language.cpp

+4
Original file line numberDiff line numberDiff line change
@@ -82,13 +82,16 @@ bool ansi_c_languaget::parse(
8282
ansi_c_parser.cpp11=false; // it's not C++
8383
ansi_c_parser.mode=config.ansi_c.mode;
8484

85+
ansi_c_scanner_init(ansi_c_parser);
86+
8587
bool result=ansi_c_parser.parse();
8688

8789
if(!result)
8890
{
8991
ansi_c_parser.set_line_no(0);
9092
ansi_c_parser.set_file(path);
9193
ansi_c_parser.in=&i_preprocessed;
94+
ansi_c_scanner_init(ansi_c_parser);
9295
result=ansi_c_parser.parse();
9396
}
9497

@@ -202,6 +205,7 @@ bool ansi_c_languaget::to_expr(
202205
ansi_c_parser.cpp98 = false; // it's not C++
203206
ansi_c_parser.cpp11 = false; // it's not C++
204207
ansi_c_parser.mode = config.ansi_c.mode;
208+
ansi_c_scanner_init(ansi_c_parser);
205209

206210
bool result=ansi_c_parser.parse();
207211

src/ansi-c/ansi_c_parser.cpp

-17
Original file line numberDiff line numberDiff line change
@@ -10,23 +10,6 @@ Author: Daniel Kroening, [email protected]
1010

1111
#include "c_storage_spec.h"
1212

13-
int yyansi_clex_init_extra(ansi_c_parsert *, void **);
14-
int yyansi_clex_destroy(void *);
15-
int yyansi_cparse(ansi_c_parsert &, void *);
16-
void yyansi_cset_debug(int, void *);
17-
18-
bool ansi_c_parsert::parse()
19-
{
20-
void *scanner;
21-
yyansi_clex_init_extra(this, &scanner);
22-
#ifdef ANSI_C_DEBUG
23-
yyansi_cset_debug(1, scanner);
24-
#endif
25-
bool parse_fail = yyansi_cparse(*this, scanner) != 0;
26-
yyansi_clex_destroy(scanner);
27-
return parse_fail;
28-
}
29-
3013
ansi_c_id_classt ansi_c_parsert::lookup(
3114
const irep_idt &base_name,
3215
irep_idt &identifier, // output

src/ansi-c/ansi_c_parser.h

+9-1
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,9 @@ Author: Daniel Kroening, [email protected]
1818
#include "ansi_c_parse_tree.h"
1919
#include "ansi_c_scope.h"
2020

21+
class ansi_c_parsert;
22+
int yyansi_cparse(ansi_c_parsert &);
23+
2124
class ansi_c_parsert:public parsert
2225
{
2326
public:
@@ -41,7 +44,10 @@ class ansi_c_parsert:public parsert
4144
scopes.push_back(scopet());
4245
}
4346

44-
bool parse() override;
47+
bool parse() override
48+
{
49+
return yyansi_cparse(*this) != 0;
50+
}
4551

4652
void clear() override
4753
{
@@ -169,4 +175,6 @@ class ansi_c_parsert:public parsert
169175
std::list<std::map<const irep_idt, bool>> pragma_cprover_stack;
170176
};
171177

178+
void ansi_c_scanner_init(ansi_c_parsert &);
179+
172180
#endif // CPROVER_ANSI_C_ANSI_C_PARSER_H

src/ansi-c/builtin_factory.cpp

+2
Original file line numberDiff line numberDiff line change
@@ -58,6 +58,8 @@ static bool convert(
5858
ansi_c_parser.cpp11=false; // it's not C++
5959
ansi_c_parser.mode=config.ansi_c.mode;
6060

61+
ansi_c_scanner_init(ansi_c_parser);
62+
6163
if(ansi_c_parser.parse())
6264
return true;
6365

0 commit comments

Comments
 (0)