Skip to content

Commit d24f773

Browse files
tautschnigtautschnig
authored
Merge pull request diffblue#2233 from thomasspriggs/global_null_message_handler
Add global null message handler
2 parents 690613d + e05dad5 commit d24f773

File tree

9 files changed

+66
-35
lines changed

9 files changed

+66
-35
lines changed

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

Lines changed: 13 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -8,9 +8,10 @@
88

99
#include "load_java_class.h"
1010

11-
#include <testing-utils/free_form_cmdline.h>
12-
#include <testing-utils/catch.hpp>
1311
#include <iostream>
12+
#include <testing-utils/catch.hpp>
13+
#include <testing-utils/free_form_cmdline.h>
14+
#include <testing-utils/message.h>
1415

1516
#include <util/config.h>
1617
#include <util/suffix.h>
@@ -94,13 +95,16 @@ symbol_tablet load_java_class(
9495
std::string filename=java_class_name + ".class";
9596

9697
// Construct a lazy_goto_modelt
97-
null_message_handlert message_handler;
9898
lazy_goto_modelt lazy_goto_model(
99-
[] (goto_model_functiont &function, const abstract_goto_modelt &model) { }, // NOLINT (*)
100-
[] (goto_modelt &goto_model) { return false; }, // NOLINT (*)
101-
[] (const irep_idt &name) { return false; },
102-
[] (const irep_idt &function_name, symbol_table_baset &symbol_table, goto_functiont &function, bool body_available) { return false; }, // NOLINT (*)
103-
message_handler);
99+
[](goto_model_functiont &function, const abstract_goto_modelt &model) {},
100+
[](goto_modelt &goto_model) { return false; },
101+
[](const irep_idt &name) { return false; },
102+
[](
103+
const irep_idt &function_name,
104+
symbol_table_baset &symbol_table,
105+
goto_functiont &function,
106+
bool body_available) { return false; },
107+
null_message_handler);
104108

105109
// Configure the path loading
106110
config.java.classpath.clear();
@@ -115,7 +119,7 @@ symbol_tablet load_java_class(
115119
std::istringstream java_code_stream("ignored");
116120

117121
// Configure the language, load the class files
118-
language.set_message_handler(message_handler);
122+
language.set_message_handler(null_message_handler);
119123
language.get_language_options(command_line);
120124
language.parse(java_code_stream, filename);
121125
language.typecheck(lazy_goto_model.symbol_table, "");

‎jbmc/unit/java_bytecode/java_bytecode_parse_lambdas/java_bytecode_parse_lambda_method_table.cpp

Lines changed: 6 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -8,13 +8,13 @@
88

99
#include <algorithm>
1010
#include <functional>
11-
#include <util/message.h>
1211
#include <util/config.h>
1312

1413
#include <java-testing-utils/require_parse_tree.h>
1514

16-
#include <testing-utils/catch.hpp>
1715
#include <java_bytecode/java_bytecode_parser.h>
16+
#include <testing-utils/catch.hpp>
17+
#include <testing-utils/message.h>
1818

1919
#include <java_bytecode/java_bytecode_parse_tree.h>
2020
#include <java_bytecode/java_types.h>
@@ -29,14 +29,13 @@ 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
{
3635
optionalt<java_bytecode_parse_treet> parse_tree = java_bytecode_parse(
3736
"./java_bytecode/java_bytecode_parse_lambdas/lambda_examples/" +
3837
compiler + "_classes/StaticLambdas.class",
39-
message_handler);
38+
null_message_handler);
4039
WHEN("Parsing that class")
4140
{
4241
REQUIRE(parse_tree);
@@ -341,13 +340,12 @@ SCENARIO(
341340
{
342341
run_test_with_compilers(
343342
[](const std::string &compiler) { // NOLINT(whitespace/braces)
344-
null_message_handlert message_handler;
345343
GIVEN("A method with local lambdas from " + compiler + " compiler.")
346344
{
347345
optionalt<java_bytecode_parse_treet> parse_tree = java_bytecode_parse(
348346
"./java_bytecode/java_bytecode_parse_lambdas/lambda_examples/" +
349347
compiler + "_classes/LocalLambdas.class",
350-
message_handler);
348+
null_message_handler);
351349
WHEN("Parsing that class")
352350
{
353351
REQUIRE(parse_tree);
@@ -648,15 +646,14 @@ SCENARIO(
648646
{
649647
run_test_with_compilers(
650648
[](const std::string &compiler) { // NOLINT(whitespace/braces)
651-
null_message_handlert message_handler;
652649
GIVEN(
653650
"A class that has lambdas as member variables from " + compiler +
654651
" compiler.")
655652
{
656653
optionalt<java_bytecode_parse_treet> parse_tree = java_bytecode_parse(
657654
"./java_bytecode/java_bytecode_parse_lambdas/lambda_examples/" +
658655
compiler + "_classes/MemberLambdas.class",
659-
message_handler);
656+
null_message_handler);
660657
WHEN("Parsing that class")
661658
{
662659
REQUIRE(parse_tree);
@@ -982,7 +979,6 @@ SCENARIO(
982979
{
983980
run_test_with_compilers(
984981
[](const std::string &compiler) { // NOLINT(whitespace/braces)
985-
null_message_handlert message_handler;
986982
GIVEN(
987983
"An inner class with member variables as lambdas that capture outer "
988984
"variables from " +
@@ -991,7 +987,7 @@ SCENARIO(
991987
optionalt<java_bytecode_parse_treet> parse_tree = java_bytecode_parse(
992988
"./java_bytecode/java_bytecode_parse_lambdas/lambda_examples/" +
993989
compiler + "_classes/OuterMemberLambdas$Inner.class",
994-
message_handler);
990+
null_message_handler);
995991
WHEN("Parsing that class")
996992
{
997993
REQUIRE(parse_tree);

‎jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -7,8 +7,9 @@
77
88
\*******************************************************************/
99

10-
#include <testing-utils/catch.hpp>
1110
#include <java-testing-utils/load_java_class.h>
11+
#include <testing-utils/catch.hpp>
12+
#include <testing-utils/message.h>
1213

1314
#include <goto-programs/goto_convert_functions.h>
1415
#include <goto-programs/remove_virtual_functions.h>
@@ -84,9 +85,8 @@ TEST_CASE(
8485
journalling_symbol_tablet symbol_table =
8586
journalling_symbol_tablet::wrap(raw_symbol_table);
8687

87-
null_message_handlert null_output;
8888
goto_functionst functions;
89-
goto_convert(symbol_table, functions, null_output);
89+
goto_convert(symbol_table, functions, null_message_handler);
9090

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

‎jbmc/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -6,8 +6,9 @@
66
77
\*******************************************************************/
88

9-
#include <testing-utils/catch.hpp>
109
#include <java-testing-utils/load_java_class.h>
10+
#include <testing-utils/catch.hpp>
11+
#include <testing-utils/message.h>
1112

1213
#include <goto-programs/goto_convert_functions.h>
1314
#include <goto-programs/remove_virtual_functions.h>
@@ -53,9 +54,8 @@ SCENARIO(
5354
WHEN("The entry point function is generated")
5455
{
5556
symbol_tablet new_table(symbol_table);
56-
null_message_handlert null_output;
5757
goto_functionst new_goto_functions;
58-
goto_convert(new_table, new_goto_functions, null_output);
58+
goto_convert(new_table, new_goto_functions, null_message_handler);
5959
remove_virtual_functions(new_table, new_goto_functions);
6060

6161
bool found_function = false;
@@ -129,7 +129,7 @@ SCENARIO(
129129
options.set_option("cover", "location");
130130
REQUIRE_FALSE(
131131
instrument_cover_goals(
132-
options, new_table, new_goto_functions, null_output));
132+
options, new_table, new_goto_functions, null_message_handler));
133133

134134
auto function = new_goto_functions.function_map.find(function_name);
135135
REQUIRE(function != new_goto_functions.function_map.end());

‎jbmc/unit/pointer-analysis/custom_value_set_analysis.cpp

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ Author: Chris Smowton, [email protected]
77
\*******************************************************************/
88

99
#include <testing-utils/catch.hpp>
10+
#include <testing-utils/message.h>
1011

1112
#include <goto-programs/goto_inline.h>
1213
#include <goto-programs/initialize_goto_model.h>
@@ -170,7 +171,6 @@ SCENARIO("test_value_set_analysis",
170171
{
171172
config.set_arch("none");
172173
config.main = "";
173-
null_message_handlert null_output;
174174
cmdlinet command_line;
175175

176176
// This classpath is the default, but the config object
@@ -181,8 +181,8 @@ SCENARIO("test_value_set_analysis",
181181

182182
register_language(new_java_bytecode_language);
183183

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

187187
null_message_handlert message_handler;
188188
remove_java_new(goto_model, message_handler);
@@ -191,7 +191,7 @@ SCENARIO("test_value_set_analysis",
191191

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

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

‎unit/json/json_parser.cpp

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -8,10 +8,10 @@
88

99
#include <json/json_parser.h>
1010
#include <testing-utils/catch.hpp>
11+
#include <testing-utils/message.h>
1112

1213
SCENARIO("Loading JSON files")
1314
{
14-
null_message_handlert message_handler;
1515
GIVEN("A invalid JSON file and a valid JSON file")
1616
{
1717
const std::string valid_json_path = "./json/valid.json";
@@ -21,7 +21,7 @@ SCENARIO("Loading JSON files")
2121
{
2222
jsont invalid_json;
2323
const auto invalid_parse_error =
24-
parse_json(invalid_json_path, message_handler, invalid_json);
24+
parse_json(invalid_json_path, null_message_handler, invalid_json);
2525
THEN("An error state should be returned")
2626
{
2727
REQUIRE(invalid_parse_error);
@@ -30,7 +30,7 @@ SCENARIO("Loading JSON files")
3030
{
3131
jsont valid_json;
3232
const auto valid_parse_error =
33-
parse_json(valid_json_path, message_handler, valid_json);
33+
parse_json(valid_json_path, null_message_handler, valid_json);
3434
THEN("The JSON file should be parsed correctly")
3535
{
3636
REQUIRE_FALSE(valid_parse_error);
@@ -45,7 +45,7 @@ SCENARIO("Loading JSON files")
4545
{
4646
jsont valid_json;
4747
const auto valid_parse_error =
48-
parse_json(valid_json_path, message_handler, valid_json);
48+
parse_json(valid_json_path, null_message_handler, valid_json);
4949
THEN("The JSON file should be parsed correctly")
5050
{
5151
REQUIRE_FALSE(valid_parse_error);
@@ -56,7 +56,7 @@ SCENARIO("Loading JSON files")
5656
{
5757
jsont invalid_json;
5858
const auto invalid_parse_error =
59-
parse_json(invalid_json_path, message_handler, invalid_json);
59+
parse_json(invalid_json_path, null_message_handler, invalid_json);
6060
THEN("An error state should be returned")
6161
{
6262
REQUIRE(invalid_parse_error);

‎unit/testing-utils/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
SRC = \
22
c_to_expr.cpp \
33
free_form_cmdline.cpp \
4+
message.cpp \
45
require_expr.cpp \
56
require_symbol.cpp \
67
run_test_with_compilers.cpp \

‎unit/testing-utils/message.cpp

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
/*******************************************************************\
2+
3+
Module: Unit test utilities
4+
5+
Author: Diffblue Ltd.
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Global instance of `null_message_handlert`.
11+
12+
#include "message.h"
13+
14+
null_message_handlert null_message_handler;

‎unit/testing-utils/message.h

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
/*******************************************************************\
2+
3+
Module: Unit test utilities
4+
5+
Author: DiffBlue Limited. All rights reserved.
6+
7+
\*******************************************************************/
8+
9+
#ifndef CPROVER_TESTING_UTILS_MESSAGE_H
10+
#define CPROVER_TESTING_UTILS_MESSAGE_H
11+
12+
#include <util/message.h>
13+
14+
extern null_message_handlert null_message_handler;
15+
16+
#endif // CPROVER_TESTING_UTILS_MESSAGE_H

0 commit comments

Comments
 (0)