Skip to content

Commit e3d28c9

Browse files
tautschnigtautschnig
committed
WIP: message handler
1 parent dec6e2e commit e3d28c9

File tree

76 files changed

+1699
-226
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

76 files changed

+1699
-226
lines changed

‎jbmc/src/java_bytecode/java_bytecode_parser.cpp

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -27,8 +27,8 @@ Author: Daniel Kroening, [email protected]
2727
class java_bytecode_parsert final : public parsert
2828
{
2929
public:
30-
explicit java_bytecode_parsert(bool skip_instructions)
31-
: skip_instructions(skip_instructions)
30+
java_bytecode_parsert(bool skip_instructions, message_handlert &message_handler)
31+
: parsert(message_handler), skip_instructions(skip_instructions)
3232
{
3333
}
3434

@@ -1809,9 +1809,8 @@ std::optional<java_bytecode_parse_treet> java_bytecode_parse(
18091809
message_handlert &message_handler,
18101810
bool skip_instructions)
18111811
{
1812-
java_bytecode_parsert java_bytecode_parser(skip_instructions);
1812+
java_bytecode_parsert java_bytecode_parser(skip_instructions, message_handler);
18131813
java_bytecode_parser.in=&istream;
1814-
java_bytecode_parser.log.set_message_handler(message_handler);
18151814

18161815
bool parser_result=java_bytecode_parser.parse();
18171816

‎jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -172,7 +172,7 @@ decision_proceduret::resultt check_sat(const exprt &expr, const namespacet &ns)
172172
info.ns = &ns;
173173
info.prop = &sat_check;
174174
info.output_xml = false;
175-
bv_refinementt solver(info);
175+
bv_refinementt solver(info, null_message_handler);
176176
solver << expr;
177177
return solver();
178178
}

‎src/ansi-c/ansi_c_language.cpp

Lines changed: 2 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -71,26 +71,22 @@ bool ansi_c_languaget::parse(
7171
ansi_c_internal_additions(code);
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();
85-
8683
bool result=ansi_c_parser.parse();
8784

8885
if(!result)
8986
{
9087
ansi_c_parser.set_line_no(0);
9188
ansi_c_parser.set_file(path);
9289
ansi_c_parser.in=&i_preprocessed;
93-
ansi_c_scanner_init();
9490
result=ansi_c_parser.parse();
9591
}
9692

@@ -205,13 +201,12 @@ bool ansi_c_languaget::to_expr(
205201

206202
// parsing
207203

208-
ansi_c_parser.clear();
204+
ansi_c_parsert ansi_c_parser(get_message_handler());
209205
ansi_c_parser.set_file(irep_idt());
210206
ansi_c_parser.in=&i_preprocessed;
211207
ansi_c_parser.log.set_message_handler(message_handler);
212208
ansi_c_parser.mode=config.ansi_c.mode;
213209
ansi_c_parser.ts_18661_3_Floatn_types=config.ansi_c.ts_18661_3_Floatn_types;
214-
ansi_c_scanner_init();
215210

216211
bool result=ansi_c_parser.parse();
217212

‎src/ansi-c/ansi_c_parser.cpp

Lines changed: 31 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,37 @@ Author: Daniel Kroening, [email protected]
1010

1111
#include "c_storage_spec.h"
1212

13-
ansi_c_parsert ansi_c_parser;
13+
void ansi_c_parser_init(ansi_c_parsert *ansi_c_parser);
14+
void ansi_c_scanner_init(ansi_c_parsert *ansi_c_parser);
15+
int yyansi_cparse();
16+
17+
bool ansi_c_parsert::parse()
18+
{
19+
clear();
20+
ansi_c_scanner_init(this);
21+
ansi_c_parser_init(this);
22+
return yyansi_cparse()!=0;
23+
}
24+
25+
void ansi_c_parsert::clear()
26+
{
27+
parsert::clear();
28+
parse_tree.clear();
29+
30+
// scanner state
31+
tag_following=false;
32+
asm_block_following=false;
33+
parenthesis_counter=0;
34+
string_literal.clear();
35+
pragma_pack.clear();
36+
37+
// set up global scope
38+
scopes.clear();
39+
scopes.push_back(scopet());
40+
41+
ansi_c_scanner_init(nullptr);
42+
ansi_c_parser_init(nullptr);
43+
}
1444

1545
ansi_c_id_classt ansi_c_parsert::lookup(
1646
const irep_idt &base_name,
@@ -73,14 +103,6 @@ void ansi_c_parsert::add_tag_with_body(irept &tag)
73103
}
74104
}
75105

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-
84106
void ansi_c_parsert::add_declarator(
85107
exprt &declaration,
86108
irept &declarator)

‎src/ansi-c/ansi_c_parser.h

Lines changed: 19 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -18,13 +18,12 @@ Author: Daniel Kroening, [email protected]
1818
#include "ansi_c_parse_tree.h"
1919
#include "ansi_c_scope.h"
2020

21-
int yyansi_cparse();
22-
2321
class ansi_c_parsert:public parsert
2422
{
2523
public:
2624
ansi_c_parse_treet parse_tree;
2725

26+
<<<<<<< HEAD
2827
ansi_c_parsert()
2928
: tag_following(false),
3029
asm_block_following(false),
@@ -34,14 +33,25 @@ class ansi_c_parsert:public parsert
3433
cpp11(false),
3534
for_has_scope(false),
3635
ts_18661_3_Floatn_types(false)
36+
=======
37+
explicit ansi_c_parsert(message_handlert &message_handler):
38+
parsert(message_handler),
39+
tag_following(false),
40+
asm_block_following(false),
41+
parenthesis_counter(0),
42+
mode(modet::NONE),
43+
cpp98(false),
44+
cpp11(false),
45+
for_has_scope(false),
46+
ts_18661_3_Floatn_types(false),
47+
Float128_type(false)
48+
>>>>>>> WIP: message handler
3749
{
3850
}
3951

40-
virtual bool parse() override
41-
{
42-
return yyansi_cparse()!=0;
43-
}
52+
bool parse() override;
4453

54+
<<<<<<< HEAD
4555
virtual void clear() override
4656
{
4757
parsert::clear();
@@ -59,6 +69,9 @@ class ansi_c_parsert:public parsert
5969
scopes.clear();
6070
scopes.push_back(scopet());
6171
}
72+
=======
73+
void clear() override;
74+
>>>>>>> WIP: message handler
6275

6376
// internal state of the scanner
6477
bool tag_following;
@@ -166,9 +179,4 @@ class ansi_c_parsert:public parsert
166179
std::list<std::map<const irep_idt, bool>> pragma_cprover_stack;
167180
};
168181

169-
extern ansi_c_parsert ansi_c_parser;
170-
171-
int yyansi_cerror(const std::string &error);
172-
void ansi_c_scanner_init();
173-
174182
#endif // CPROVER_ANSI_C_ANSI_C_PARSER_H

‎src/ansi-c/builtin_factory.cpp

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,7 @@ 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;
5353
ansi_c_parser.log.set_message_handler(message_handler);
@@ -56,8 +56,6 @@ static bool convert(
5656
ansi_c_parser.cpp11=false; // it's not C++
5757
ansi_c_parser.mode=config.ansi_c.mode;
5858

59-
ansi_c_scanner_init();
60-
6159
if(ansi_c_parser.parse())
6260
return true;
6361

‎src/ansi-c/parser.y

Lines changed: 9 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -13,12 +13,19 @@
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();
21-
extern char *yyansi_ctext;
21+
int yyansi_cerror(const std::string &error);
22+
23+
static ansi_c_parsert *ansi_c_parser;
24+
25+
void ansi_c_parser_init(ansi_c_parsert *_ansi_c_parser)
26+
{
27+
ansi_c_parser = _ansi_c_parser;
28+
}
2229

2330
#include "parser_static.inc"
2431

‎src/ansi-c/scanner.l

Lines changed: 16 additions & 3 deletions
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
@@ -52,6 +52,10 @@ extern int yyansi_cdebug;
5252
#define loc() \
5353
{ newstack(yyansi_clval); PARSER.set_source_location(parser_stack(yyansi_clval)); }
5454

55+
static ansi_c_parsert *ansi_c_parser;
56+
57+
int yyansi_cerror(const std::string &error);
58+
5559
int make_identifier()
5660
{
5761
loc();
@@ -265,8 +269,9 @@ enable_or_disable ("enable"|"disable")
265269
%x OTHER_PRAGMA
266270

267271
%{
268-
void ansi_c_scanner_init()
272+
void ansi_c_scanner_init(ansi_c_parsert *_ansi_c_parser)
269273
{
274+
ansi_c_parser = _ansi_c_parser;
270275
#ifdef ANSI_C_DEBUG
271276
yyansi_cdebug=1;
272277
#endif
@@ -277,7 +282,8 @@ void ansi_c_scanner_init()
277282

278283
%%
279284

280-
<INITIAL>.|\n { BEGIN(GRAMMAR);
285+
<INITIAL>.|\n { PRECONDITION(ansi_c_parser);
286+
BEGIN(GRAMMAR);
281287
yyless(0); /* start again with this character */
282288
}
283289

@@ -1815,3 +1821,10 @@ __decltype { if(PARSER.cpp98 &&
18151821
%%
18161822

18171823
int yywrap() { return 1; }
1824+
1825+
int yyansi_cerror(const std::string &error)
1826+
{
1827+
PRECONDITION(ansi_c_parser);
1828+
ansi_c_parser->parse_error(error, yyansi_ctext);
1829+
return 0;
1830+
}

‎src/assembler/assembler_parser.cpp

Lines changed: 16 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -8,12 +8,25 @@ Author: Daniel Kroening, [email protected]
88

99
#include "assembler_parser.h"
1010

11+
<<<<<<< HEAD
1112
assembler_parsert assembler_parser;
1213

1314
extern char *yyassemblertext;
15+
=======
16+
int yyassemblerlex();
17+
void assembler_scanner_init(assembler_parsert *assembler_parser);
1418

15-
int yyassemblererror(const std::string &error)
19+
bool assembler_parsert::parse()
1620
{
17-
assembler_parser.parse_error(error, yyassemblertext);
18-
return 0;
21+
assembler_scanner_init(this);
22+
yyassemblerlex();
23+
return false;
24+
}
25+
>>>>>>> WIP: message handler
26+
27+
void assembler_parsert::clear()
28+
{
29+
parsert::clear();
30+
instructions.clear();
31+
assembler_scanner_init(nullptr);
1932
}

‎src/assembler/assembler_parser.h

Lines changed: 7 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -11,12 +11,15 @@ Author: Daniel Kroening, [email protected]
1111
#define CPROVER_ASSEMBLER_ASSEMBLER_PARSER_H
1212

1313
#include <util/parser.h>
14+
<<<<<<< HEAD
1415

1516
#include <list>
1617

1718
int yyassemblerlex();
1819
int yyassemblererror(const std::string &error);
1920
void assembler_scanner_init();
21+
=======
22+
>>>>>>> WIP: message handler
2023

2124
class assembler_parsert:public parsert
2225
{
@@ -37,24 +40,14 @@ class assembler_parsert:public parsert
3740
instructions.push_back(instructiont());
3841
}
3942

40-
assembler_parsert()
43+
explicit assembler_parsert(message_handlert &message_handler)
44+
: parsert(message_handler)
4145
{
4246
}
4347

44-
virtual bool parse()
45-
{
46-
yyassemblerlex();
47-
return false;
48-
}
48+
bool parse() override;
4949

50-
virtual void clear()
51-
{
52-
parsert::clear();
53-
instructions.clear();
54-
// assembler_scanner_init();
55-
}
50+
void clear() override;
5651
};
5752

58-
extern assembler_parsert assembler_parser;
59-
6053
#endif // CPROVER_ASSEMBLER_ASSEMBLER_PARSER_H

0 commit comments

Comments
 (0)