Skip to content

Commit 953e750

Browse files
committed
Use global null_message_handlert instead of duplicates.
1 parent 54929ba commit 953e750

File tree

12 files changed

+21
-37
lines changed

12 files changed

+21
-37
lines changed

jbmc/src/java_bytecode/java_object_factory.cpp

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1055,10 +1055,9 @@ void java_object_factoryt::gen_nondet_struct_init(
10551055
// passes can easily recognise leaves no uninitialised state behind.
10561056

10571057
// This code mirrors the `remove_java_new` pass:
1058-
null_message_handlert nullout;
10591058
exprt zero_object=
10601059
zero_initializer(
1061-
struct_type, source_locationt(), ns, nullout);
1060+
struct_type, source_locationt(), ns, null_message_handler);
10621061
irep_idt qualified_clsid = "java::" + id2string(class_identifier);
10631062
set_class_identifier(
10641063
to_struct_expr(zero_object), ns, symbol_typet(qualified_clsid));

jbmc/unit/java-testing-utils/load_java_class.cpp

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -94,13 +94,12 @@ symbol_tablet load_java_class(
9494
std::string filename=java_class_name + ".class";
9595

9696
// Construct a lazy_goto_modelt
97-
null_message_handlert message_handler;
9897
lazy_goto_modelt lazy_goto_model(
9998
[] (goto_model_functiont &function, const abstract_goto_modelt &model) { }, // NOLINT (*)
10099
[] (goto_modelt &goto_model) { return false; }, // NOLINT (*)
101100
[] (const irep_idt &name) { return false; },
102101
[] (const irep_idt &function_name, symbol_table_baset &symbol_table, goto_functiont &function, bool body_available) { return false; }, // NOLINT (*)
103-
message_handler);
102+
null_message_handler);
104103

105104
// Configure the path loading
106105
config.java.classpath.clear();
@@ -115,7 +114,7 @@ symbol_tablet load_java_class(
115114
std::istringstream java_code_stream("ignored");
116115

117116
// Configure the language, load the class files
118-
language.set_message_handler(message_handler);
117+
language.set_message_handler(null_message_handler);
119118
language.get_language_options(command_line);
120119
language.parse(java_code_stream, filename);
121120
language.typecheck(lazy_goto_model.symbol_table, "");

jbmc/unit/java_bytecode/java_bytecode_parse_lambdas/java_bytecode_parse_lambda_method_table.cpp

Lines changed: 4 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,6 @@ SCENARIO(
2929
{
3030
// NOLINTNEXTLINE(whitespace/braces)
3131
run_test_with_compilers([](const std::string &compiler) {
32-
null_message_handlert message_handler;
3332
GIVEN(
3433
"A class with a static lambda variables from " + compiler + " compiler.")
3534
{
@@ -38,7 +37,7 @@ SCENARIO(
3837
"./java_bytecode/java_bytecode_parse_lambdas/lambda_examples/" +
3938
compiler + "_classes/StaticLambdas.class",
4039
parse_tree,
41-
message_handler);
40+
null_message_handler);
4241
WHEN("Parsing that class")
4342
{
4443
REQUIRE(parse_tree.loading_successful);
@@ -342,15 +341,14 @@ SCENARIO(
342341
{
343342
run_test_with_compilers(
344343
[](const std::string &compiler) { // NOLINT(whitespace/braces)
345-
null_message_handlert message_handler;
346344
GIVEN("A method with local lambdas from " + compiler + " compiler.")
347345
{
348346
java_bytecode_parse_treet parse_tree;
349347
java_bytecode_parse(
350348
"./java_bytecode/java_bytecode_parse_lambdas/lambda_examples/" +
351349
compiler + "_classes/LocalLambdas.class",
352350
parse_tree,
353-
message_handler);
351+
null_message_handler);
354352
WHEN("Parsing that class")
355353
{
356354
REQUIRE(parse_tree.loading_successful);
@@ -650,7 +648,6 @@ SCENARIO(
650648
{
651649
run_test_with_compilers(
652650
[](const std::string &compiler) { // NOLINT(whitespace/braces)
653-
null_message_handlert message_handler;
654651
GIVEN(
655652
"A class that has lambdas as member variables from " + compiler +
656653
" compiler.")
@@ -660,7 +657,7 @@ SCENARIO(
660657
"./java_bytecode/java_bytecode_parse_lambdas/lambda_examples/" +
661658
compiler + "_classes/MemberLambdas.class",
662659
parse_tree,
663-
message_handler);
660+
null_message_handler);
664661
WHEN("Parsing that class")
665662
{
666663
REQUIRE(parse_tree.loading_successful);
@@ -985,7 +982,6 @@ SCENARIO(
985982
{
986983
run_test_with_compilers(
987984
[](const std::string &compiler) { // NOLINT(whitespace/braces)
988-
null_message_handlert message_handler;
989985
GIVEN(
990986
"An inner class with member variables as lambdas that capture outer "
991987
"variables from " +
@@ -996,7 +992,7 @@ SCENARIO(
996992
"./java_bytecode/java_bytecode_parse_lambdas/lambda_examples/" +
997993
compiler + "_classes/OuterMemberLambdas$Inner.class",
998994
parse_tree,
999-
message_handler);
995+
null_message_handler);
1000996
WHEN("Parsing that class")
1001997
{
1002998
REQUIRE(parse_tree.loading_successful);

jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -84,9 +84,8 @@ TEST_CASE(
8484
journalling_symbol_tablet symbol_table =
8585
journalling_symbol_tablet::wrap(raw_symbol_table);
8686

87-
null_message_handlert null_output;
8887
goto_functionst functions;
89-
goto_convert(symbol_table, functions, null_output);
88+
goto_convert(symbol_table, functions, null_message_handler);
9089

9190
const std::string function_name = "java::Main.replaceNondet:()V";
9291
goto_functionst::goto_functiont &goto_function =

jbmc/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -53,9 +53,8 @@ SCENARIO(
5353
WHEN("The entry point function is generated")
5454
{
5555
symbol_tablet new_table(symbol_table);
56-
null_message_handlert null_output;
5756
goto_functionst new_goto_functions;
58-
goto_convert(new_table, new_goto_functions, null_output);
57+
goto_convert(new_table, new_goto_functions, null_message_handler);
5958
remove_virtual_functions(new_table, new_goto_functions);
6059

6160
bool found_function = false;
@@ -129,7 +128,7 @@ SCENARIO(
129128
options.set_option("cover", "location");
130129
REQUIRE_FALSE(
131130
instrument_cover_goals(
132-
options, new_table, new_goto_functions, null_output));
131+
options, new_table, new_goto_functions, null_message_handler));
133132

134133
auto function = new_goto_functions.function_map.find(function_name);
135134
REQUIRE(function != new_goto_functions.function_map.end());

jbmc/unit/pointer-analysis/custom_value_set_analysis.cpp

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -170,7 +170,6 @@ SCENARIO("test_value_set_analysis",
170170
{
171171
config.set_arch("none");
172172
config.main = "";
173-
null_message_handlert null_output;
174173
cmdlinet command_line;
175174

176175
// This classpath is the default, but the config object
@@ -182,7 +181,7 @@ SCENARIO("test_value_set_analysis",
182181
register_language(new_java_bytecode_language);
183182

184183
goto_modelt goto_model=
185-
initialize_goto_model(command_line, null_output);
184+
initialize_goto_model(command_line, null_message_handler);
186185

187186
null_message_handlert message_handler;
188187
remove_java_new(goto_model, message_handler);
@@ -191,7 +190,7 @@ SCENARIO("test_value_set_analysis",
191190

192191
// Fully inline the test program, to avoid VSA conflating
193192
// constructor callsites confusing the results we're trying to check:
194-
goto_function_inline(goto_model, TEST_FUNCTION_NAME, null_output);
193+
goto_function_inline(goto_model, TEST_FUNCTION_NAME, null_message_handler);
195194

196195
const goto_programt &test_function=
197196
goto_model.goto_functions.function_map.at(TEST_PREFIX "test:()V").body;

src/cbmc/xml_interface.cpp

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -22,10 +22,9 @@ void xml_interfacet::get_xml_options(cmdlinet &cmdline)
2222
{
2323
if(cmdline.isset("xml-interface"))
2424
{
25-
null_message_handlert message_handler;
2625
xmlt xml;
2726

28-
parse_xml(std::cin, "", message_handler, xml);
27+
parse_xml(std::cin, "", null_message_handler, xml);
2928

3029
get_xml_options(xml, cmdline);
3130

src/goto-instrument/wmm/goto2graph.cpp

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1303,10 +1303,9 @@ bool instrumentert::is_cfg_spurious(const event_grapht::critical_cyclet &cyc)
13031303
goto_functionst this_interleaving;
13041304
this_interleaving.function_map=std::move(map);
13051305
optionst no_option;
1306-
null_message_handlert no_message;
13071306

13081307
#if 0
1309-
bmct bmc(no_option, symbol_table, no_message);
1308+
bmct bmc(no_option, symbol_table, null_message_handler);
13101309

13111310
bool is_spurious=bmc.run(this_interleaving);
13121311

src/goto-symex/symex_builtin_functions.cpp

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -168,13 +168,12 @@ void goto_symext::symex_allocate(
168168

169169
if(!zero_init.is_zero() && !zero_init.is_false())
170170
{
171-
null_message_handlert null_message;
172171
exprt zero_value=
173172
zero_initializer(
174173
object_type,
175174
code.source_location(),
176175
ns,
177-
null_message);
176+
null_message_handler);
178177

179178
if(zero_value.is_not_nil())
180179
{

src/langapi/language_util.cpp

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -75,7 +75,6 @@ exprt to_expr(
7575
{
7676
std::unique_ptr<languaget> p(get_language_from_identifier(ns, identifier));
7777

78-
null_message_handlert null_message_handler;
7978
p->set_message_handler(null_message_handler);
8079

8180
const symbolt &symbol=ns.lookup(identifier);

src/xmllang/graphml.cpp

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -186,10 +186,9 @@ bool read_graphml(
186186
graphmlt &dest,
187187
graphmlt::node_indext &entry)
188188
{
189-
null_message_handlert message_handler;
190189
xmlt xml;
191190

192-
if(parse_xml(is, "", message_handler, xml))
191+
if(parse_xml(is, "", null_message_handler, xml))
193192
return true;
194193

195194
return build_graph(xml, dest, entry);
@@ -200,10 +199,9 @@ bool read_graphml(
200199
graphmlt &dest,
201200
graphmlt::node_indext &entry)
202201
{
203-
null_message_handlert message_handler;
204202
xmlt xml;
205203

206-
if(parse_xml(filename, message_handler, xml))
204+
if(parse_xml(filename, null_message_handler, xml))
207205
return true;
208206

209207
return build_graph(xml, dest, entry);

unit/json/json_parser.cpp

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,6 @@
1111

1212
SCENARIO("Loading JSON files")
1313
{
14-
null_message_handlert message_handler;
1514
GIVEN("A invalid JSON file and a valid JSON file")
1615
{
1716
const std::string valid_json_path = "./json/valid.json";
@@ -21,7 +20,7 @@ SCENARIO("Loading JSON files")
2120
{
2221
jsont invalid_json;
2322
const auto invalid_parse_error =
24-
parse_json(invalid_json_path, message_handler, invalid_json);
23+
parse_json(invalid_json_path, null_message_handler, invalid_json);
2524
THEN("An error state should be returned")
2625
{
2726
REQUIRE(invalid_parse_error);
@@ -30,7 +29,7 @@ SCENARIO("Loading JSON files")
3029
{
3130
jsont valid_json;
3231
const auto valid_parse_error =
33-
parse_json(valid_json_path, message_handler, valid_json);
32+
parse_json(valid_json_path, null_message_handler, valid_json);
3433
THEN("The JSON file should be parsed correctly")
3534
{
3635
REQUIRE_FALSE(valid_parse_error);
@@ -45,7 +44,7 @@ SCENARIO("Loading JSON files")
4544
{
4645
jsont valid_json;
4746
const auto valid_parse_error =
48-
parse_json(valid_json_path, message_handler, valid_json);
47+
parse_json(valid_json_path, null_message_handler, valid_json);
4948
THEN("The JSON file should be parsed correctly")
5049
{
5150
REQUIRE_FALSE(valid_parse_error);
@@ -56,7 +55,7 @@ SCENARIO("Loading JSON files")
5655
{
5756
jsont invalid_json;
5857
const auto invalid_parse_error =
59-
parse_json(invalid_json_path, message_handler, invalid_json);
58+
parse_json(invalid_json_path, null_message_handler, invalid_json);
6059
THEN("An error state should be returned")
6160
{
6261
REQUIRE(invalid_parse_error);

0 commit comments

Comments
 (0)