Skip to content

Commit cf789e9

Browse files
committed
ansi_c_parsert: construct with message handler
This both avoids an object of static lifetime as well as it fixes the (transitive) use of the deprecated messaget() constructor.
1 parent d2ca83b commit cf789e9

File tree

7 files changed

+48
-43
lines changed

7 files changed

+48
-43
lines changed

src/ansi-c/ansi_c_language.cpp

+5-7
Original file line numberDiff line numberDiff line change
@@ -71,17 +71,16 @@ bool ansi_c_languaget::parse(
7171
ansi_c_internal_additions(code, config.ansi_c.ts_18661_3_Floatn_types);
7272
std::istringstream codestr(code);
7373

74-
ansi_c_parser.clear();
74+
ansi_c_parsert ansi_c_parser{message_handler};
7575
ansi_c_parser.set_file(ID_built_in);
7676
ansi_c_parser.in=&codestr;
77-
ansi_c_parser.log.set_message_handler(message_handler);
7877
ansi_c_parser.for_has_scope=config.ansi_c.for_has_scope;
7978
ansi_c_parser.ts_18661_3_Floatn_types=config.ansi_c.ts_18661_3_Floatn_types;
8079
ansi_c_parser.cpp98=false; // it's not C++
8180
ansi_c_parser.cpp11=false; // it's not C++
8281
ansi_c_parser.mode=config.ansi_c.mode;
8382

84-
ansi_c_scanner_init();
83+
ansi_c_scanner_init(ansi_c_parser);
8584

8685
bool result=ansi_c_parser.parse();
8786

@@ -90,7 +89,7 @@ bool ansi_c_languaget::parse(
9089
ansi_c_parser.set_line_no(0);
9190
ansi_c_parser.set_file(path);
9291
ansi_c_parser.in=&i_preprocessed;
93-
ansi_c_scanner_init();
92+
ansi_c_scanner_init(ansi_c_parser);
9493
result=ansi_c_parser.parse();
9594
}
9695

@@ -197,13 +196,12 @@ bool ansi_c_languaget::to_expr(
197196

198197
// parsing
199198

200-
ansi_c_parser.clear();
199+
ansi_c_parsert ansi_c_parser{message_handler};
201200
ansi_c_parser.set_file(irep_idt());
202201
ansi_c_parser.in=&i_preprocessed;
203-
ansi_c_parser.log.set_message_handler(message_handler);
204202
ansi_c_parser.mode=config.ansi_c.mode;
205203
ansi_c_parser.ts_18661_3_Floatn_types=config.ansi_c.ts_18661_3_Floatn_types;
206-
ansi_c_scanner_init();
204+
ansi_c_scanner_init(ansi_c_parser);
207205

208206
bool result=ansi_c_parser.parse();
209207

src/ansi-c/ansi_c_parser.cpp

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

1111
#include "c_storage_spec.h"
1212

13-
ansi_c_parsert ansi_c_parser;
14-
1513
ansi_c_id_classt ansi_c_parsert::lookup(
1614
const irep_idt &base_name,
1715
irep_idt &identifier, // output
@@ -73,14 +71,6 @@ void ansi_c_parsert::add_tag_with_body(irept &tag)
7371
}
7472
}
7573

76-
extern char *yyansi_ctext;
77-
78-
int yyansi_cerror(const std::string &error)
79-
{
80-
ansi_c_parser.parse_error(error, yyansi_ctext);
81-
return 0;
82-
}
83-
8474
void ansi_c_parsert::add_declarator(
8575
exprt &declaration,
8676
irept &declarator)

src/ansi-c/ansi_c_parser.h

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

21-
int yyansi_cparse();
21+
class ansi_c_parsert;
22+
int yyansi_cparse(ansi_c_parsert &);
2223

2324
class ansi_c_parsert:public parsert
2425
{
2526
public:
2627
ansi_c_parse_treet parse_tree;
2728

28-
ansi_c_parsert()
29-
: tag_following(false),
29+
explicit ansi_c_parsert(message_handlert &message_handler)
30+
: parsert(message_handler),
31+
tag_following(false),
3032
asm_block_following(false),
3133
parenthesis_counter(0),
3234
mode(modet::NONE),
@@ -35,11 +37,14 @@ class ansi_c_parsert:public parsert
3537
for_has_scope(false),
3638
ts_18661_3_Floatn_types(false)
3739
{
40+
// set up global scope
41+
scopes.clear();
42+
scopes.push_back(scopet());
3843
}
3944

4045
virtual bool parse() override
4146
{
42-
return yyansi_cparse()!=0;
47+
return yyansi_cparse(*this) != 0;
4348
}
4449

4550
virtual void clear() override
@@ -166,9 +171,6 @@ class ansi_c_parsert:public parsert
166171
std::list<std::map<const irep_idt, bool>> pragma_cprover_stack;
167172
};
168173

169-
extern ansi_c_parsert ansi_c_parser;
170-
171-
int yyansi_cerror(const std::string &error);
172-
void ansi_c_scanner_init();
174+
void ansi_c_scanner_init(ansi_c_parsert &);
173175

174176
#endif // CPROVER_ANSI_C_ANSI_C_PARSER_H

src/ansi-c/builtin_factory.cpp

+2-3
Original file line numberDiff line numberDiff line change
@@ -47,16 +47,15 @@ static bool convert(
4747
{
4848
std::istringstream in(s.str());
4949

50-
ansi_c_parser.clear();
50+
ansi_c_parsert ansi_c_parser{message_handler};
5151
ansi_c_parser.set_file(ID_built_in);
5252
ansi_c_parser.in=&in;
53-
ansi_c_parser.log.set_message_handler(message_handler);
5453
ansi_c_parser.for_has_scope=config.ansi_c.for_has_scope;
5554
ansi_c_parser.cpp98=false; // it's not C++
5655
ansi_c_parser.cpp11=false; // it's not C++
5756
ansi_c_parser.mode=config.ansi_c.mode;
5857

59-
ansi_c_scanner_init();
58+
ansi_c_scanner_init(ansi_c_parser);
6059

6160
if(ansi_c_parser.parse())
6261
return true;

src/ansi-c/parser.y

+15-1
Original file line numberDiff line numberDiff line change
@@ -13,13 +13,27 @@
1313
#ifdef ANSI_C_DEBUG
1414
#define YYDEBUG 1
1515
#endif
16-
#define PARSER ansi_c_parser
16+
#define PARSER (*ansi_c_parser)
1717

1818
#include "ansi_c_parser.h"
1919

2020
int yyansi_clex();
2121
extern char *yyansi_ctext;
2222

23+
static ansi_c_parsert *ansi_c_parser;
24+
int yyansi_cparse(void);
25+
int yyansi_cparse(ansi_c_parsert &_ansi_c_parser)
26+
{
27+
ansi_c_parser = &_ansi_c_parser;
28+
return yyansi_cparse();
29+
}
30+
31+
int yyansi_cerror(const std::string &error)
32+
{
33+
ansi_c_parser->parse_error(error, yyansi_ctext);
34+
return 0;
35+
}
36+
2337
#include "parser_static.inc"
2438

2539
#include "literals/convert_integer_literal.h"

src/ansi-c/scanner.l

+14-12
Original file line numberDiff line numberDiff line change
@@ -38,7 +38,7 @@ static int isatty(int) { return 0; }
3838
#include "literals/convert_string_literal.h"
3939
#include "literals/unescape_string.h"
4040

41-
#define PARSER ansi_c_parser
41+
#define PARSER (*ansi_c_parser)
4242
#define YYSTYPE unsigned
4343
#undef ECHO
4444
#define ECHO
@@ -49,6 +49,19 @@ static int isatty(int) { return 0; }
4949
extern int yyansi_cdebug;
5050
#endif
5151

52+
static ansi_c_parsert *ansi_c_parser;
53+
void ansi_c_scanner_init(ansi_c_parsert &_ansi_c_parser)
54+
{
55+
#ifdef ANSI_C_DEBUG
56+
yyansi_cdebug=1;
57+
#endif
58+
ansi_c_parser = &_ansi_c_parser;
59+
YY_FLUSH_BUFFER;
60+
BEGIN(0);
61+
}
62+
63+
int yyansi_cerror(const std::string &error);
64+
5265
#define loc() \
5366
{ newstack(yyansi_clval); PARSER.set_source_location(parser_stack(yyansi_clval)); }
5467

@@ -264,17 +277,6 @@ enable_or_disable ("enable"|"disable")
264277
%x CPROVER_PRAGMA
265278
%x OTHER_PRAGMA
266279

267-
%{
268-
void ansi_c_scanner_init()
269-
{
270-
#ifdef ANSI_C_DEBUG
271-
yyansi_cdebug=1;
272-
#endif
273-
YY_FLUSH_BUFFER;
274-
BEGIN(0);
275-
}
276-
%}
277-
278280
%%
279281

280282
<INITIAL>.|\n { BEGIN(GRAMMAR);

src/goto-instrument/contracts/contracts_wrangler.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -139,11 +139,11 @@ void contracts_wranglert::mangle(
139139

140140
// Parse the fake function.
141141
std::istringstream is(pr.str());
142-
ansi_c_parser.clear();
142+
ansi_c_parsert ansi_c_parser{message_handler};
143143
ansi_c_parser.set_line_no(0);
144144
ansi_c_parser.set_file("<predicate>");
145145
ansi_c_parser.in = &is;
146-
ansi_c_scanner_init();
146+
ansi_c_scanner_init(ansi_c_parser);
147147
ansi_c_parser.parse();
148148

149149
// Extract the invariants from prase_tree.

0 commit comments

Comments
 (0)