diff --git a/jbmc/unit/java-testing-utils/load_java_class.cpp b/jbmc/unit/java-testing-utils/load_java_class.cpp index c6d9c1553fb..29d303a1605 100644 --- a/jbmc/unit/java-testing-utils/load_java_class.cpp +++ b/jbmc/unit/java-testing-utils/load_java_class.cpp @@ -8,9 +8,10 @@ #include "load_java_class.h" -#include -#include #include +#include +#include +#include #include #include @@ -94,13 +95,16 @@ symbol_tablet load_java_class( std::string filename=java_class_name + ".class"; // Construct a lazy_goto_modelt - null_message_handlert message_handler; lazy_goto_modelt lazy_goto_model( - [] (goto_model_functiont &function, const abstract_goto_modelt &model) { }, // NOLINT (*) - [] (goto_modelt &goto_model) { return false; }, // NOLINT (*) - [] (const irep_idt &name) { return false; }, - [] (const irep_idt &function_name, symbol_table_baset &symbol_table, goto_functiont &function, bool body_available) { return false; }, // NOLINT (*) - message_handler); + [](goto_model_functiont &function, const abstract_goto_modelt &model) {}, + [](goto_modelt &goto_model) { return false; }, + [](const irep_idt &name) { return false; }, + []( + const irep_idt &function_name, + symbol_table_baset &symbol_table, + goto_functiont &function, + bool body_available) { return false; }, + null_message_handler); // Configure the path loading config.java.classpath.clear(); @@ -115,7 +119,7 @@ symbol_tablet load_java_class( std::istringstream java_code_stream("ignored"); // Configure the language, load the class files - language.set_message_handler(message_handler); + language.set_message_handler(null_message_handler); language.get_language_options(command_line); language.parse(java_code_stream, filename); language.typecheck(lazy_goto_model.symbol_table, ""); diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_lambdas/java_bytecode_parse_lambda_method_table.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_lambdas/java_bytecode_parse_lambda_method_table.cpp index ad4fd25a9c8..8bbbdd3aba6 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_parse_lambdas/java_bytecode_parse_lambda_method_table.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_parse_lambdas/java_bytecode_parse_lambda_method_table.cpp @@ -8,13 +8,13 @@ #include #include -#include #include #include -#include #include +#include +#include #include #include @@ -29,14 +29,13 @@ SCENARIO( { // NOLINTNEXTLINE(whitespace/braces) run_test_with_compilers([](const std::string &compiler) { - null_message_handlert message_handler; GIVEN( "A class with a static lambda variables from " + compiler + " compiler.") { optionalt parse_tree = java_bytecode_parse( "./java_bytecode/java_bytecode_parse_lambdas/lambda_examples/" + compiler + "_classes/StaticLambdas.class", - message_handler); + null_message_handler); WHEN("Parsing that class") { REQUIRE(parse_tree); @@ -341,13 +340,12 @@ SCENARIO( { run_test_with_compilers( [](const std::string &compiler) { // NOLINT(whitespace/braces) - null_message_handlert message_handler; GIVEN("A method with local lambdas from " + compiler + " compiler.") { optionalt parse_tree = java_bytecode_parse( "./java_bytecode/java_bytecode_parse_lambdas/lambda_examples/" + compiler + "_classes/LocalLambdas.class", - message_handler); + null_message_handler); WHEN("Parsing that class") { REQUIRE(parse_tree); @@ -648,7 +646,6 @@ SCENARIO( { run_test_with_compilers( [](const std::string &compiler) { // NOLINT(whitespace/braces) - null_message_handlert message_handler; GIVEN( "A class that has lambdas as member variables from " + compiler + " compiler.") @@ -656,7 +653,7 @@ SCENARIO( optionalt parse_tree = java_bytecode_parse( "./java_bytecode/java_bytecode_parse_lambdas/lambda_examples/" + compiler + "_classes/MemberLambdas.class", - message_handler); + null_message_handler); WHEN("Parsing that class") { REQUIRE(parse_tree); @@ -982,7 +979,6 @@ SCENARIO( { run_test_with_compilers( [](const std::string &compiler) { // NOLINT(whitespace/braces) - null_message_handlert message_handler; GIVEN( "An inner class with member variables as lambdas that capture outer " "variables from " + @@ -991,7 +987,7 @@ SCENARIO( optionalt parse_tree = java_bytecode_parse( "./java_bytecode/java_bytecode_parse_lambdas/lambda_examples/" + compiler + "_classes/OuterMemberLambdas$Inner.class", - message_handler); + null_message_handler); WHEN("Parsing that class") { REQUIRE(parse_tree); diff --git a/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp b/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp index deea0406337..3011b7c7282 100644 --- a/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp +++ b/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp @@ -7,8 +7,9 @@ \*******************************************************************/ -#include #include +#include +#include #include #include @@ -84,9 +85,8 @@ TEST_CASE( journalling_symbol_tablet symbol_table = journalling_symbol_tablet::wrap(raw_symbol_table); - null_message_handlert null_output; goto_functionst functions; - goto_convert(symbol_table, functions, null_output); + goto_convert(symbol_table, functions, null_message_handler); const std::string function_name = "java::Main.replaceNondet:()V"; goto_functionst::goto_functiont &goto_function = diff --git a/jbmc/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp b/jbmc/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp index 8a2760c96e7..003f866f5f4 100644 --- a/jbmc/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp +++ b/jbmc/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp @@ -6,8 +6,9 @@ \*******************************************************************/ -#include #include +#include +#include #include #include @@ -53,9 +54,8 @@ SCENARIO( WHEN("The entry point function is generated") { symbol_tablet new_table(symbol_table); - null_message_handlert null_output; goto_functionst new_goto_functions; - goto_convert(new_table, new_goto_functions, null_output); + goto_convert(new_table, new_goto_functions, null_message_handler); remove_virtual_functions(new_table, new_goto_functions); bool found_function = false; @@ -129,7 +129,7 @@ SCENARIO( options.set_option("cover", "location"); REQUIRE_FALSE( instrument_cover_goals( - options, new_table, new_goto_functions, null_output)); + options, new_table, new_goto_functions, null_message_handler)); auto function = new_goto_functions.function_map.find(function_name); REQUIRE(function != new_goto_functions.function_map.end()); diff --git a/jbmc/unit/pointer-analysis/custom_value_set_analysis.cpp b/jbmc/unit/pointer-analysis/custom_value_set_analysis.cpp index 01791c36528..4ce2e21c530 100644 --- a/jbmc/unit/pointer-analysis/custom_value_set_analysis.cpp +++ b/jbmc/unit/pointer-analysis/custom_value_set_analysis.cpp @@ -7,6 +7,7 @@ Author: Chris Smowton, chris@smowton.net \*******************************************************************/ #include +#include #include #include @@ -170,7 +171,6 @@ SCENARIO("test_value_set_analysis", { config.set_arch("none"); config.main = ""; - null_message_handlert null_output; cmdlinet command_line; // This classpath is the default, but the config object @@ -181,8 +181,8 @@ SCENARIO("test_value_set_analysis", register_language(new_java_bytecode_language); - goto_modelt goto_model= - initialize_goto_model(command_line, null_output); + goto_modelt goto_model = + initialize_goto_model(command_line, null_message_handler); null_message_handlert message_handler; remove_java_new(goto_model, message_handler); @@ -191,7 +191,7 @@ SCENARIO("test_value_set_analysis", // Fully inline the test program, to avoid VSA conflating // constructor callsites confusing the results we're trying to check: - goto_function_inline(goto_model, TEST_FUNCTION_NAME, null_output); + goto_function_inline(goto_model, TEST_FUNCTION_NAME, null_message_handler); const goto_programt &test_function= goto_model.goto_functions.function_map.at(TEST_PREFIX "test:()V").body; diff --git a/unit/json/json_parser.cpp b/unit/json/json_parser.cpp index 0ab1d73bfc4..233ad460e9c 100644 --- a/unit/json/json_parser.cpp +++ b/unit/json/json_parser.cpp @@ -8,10 +8,10 @@ #include #include +#include SCENARIO("Loading JSON files") { - null_message_handlert message_handler; GIVEN("A invalid JSON file and a valid JSON file") { const std::string valid_json_path = "./json/valid.json"; @@ -21,7 +21,7 @@ SCENARIO("Loading JSON files") { jsont invalid_json; const auto invalid_parse_error = - parse_json(invalid_json_path, message_handler, invalid_json); + parse_json(invalid_json_path, null_message_handler, invalid_json); THEN("An error state should be returned") { REQUIRE(invalid_parse_error); @@ -30,7 +30,7 @@ SCENARIO("Loading JSON files") { jsont valid_json; const auto valid_parse_error = - parse_json(valid_json_path, message_handler, valid_json); + parse_json(valid_json_path, null_message_handler, valid_json); THEN("The JSON file should be parsed correctly") { REQUIRE_FALSE(valid_parse_error); @@ -45,7 +45,7 @@ SCENARIO("Loading JSON files") { jsont valid_json; const auto valid_parse_error = - parse_json(valid_json_path, message_handler, valid_json); + parse_json(valid_json_path, null_message_handler, valid_json); THEN("The JSON file should be parsed correctly") { REQUIRE_FALSE(valid_parse_error); @@ -56,7 +56,7 @@ SCENARIO("Loading JSON files") { jsont invalid_json; const auto invalid_parse_error = - parse_json(invalid_json_path, message_handler, invalid_json); + parse_json(invalid_json_path, null_message_handler, invalid_json); THEN("An error state should be returned") { REQUIRE(invalid_parse_error); diff --git a/unit/testing-utils/Makefile b/unit/testing-utils/Makefile index 37519706952..c6d0e6ddf5f 100644 --- a/unit/testing-utils/Makefile +++ b/unit/testing-utils/Makefile @@ -1,6 +1,7 @@ SRC = \ c_to_expr.cpp \ free_form_cmdline.cpp \ + message.cpp \ require_expr.cpp \ require_symbol.cpp \ run_test_with_compilers.cpp \ diff --git a/unit/testing-utils/message.cpp b/unit/testing-utils/message.cpp new file mode 100644 index 00000000000..896a91a1ead --- /dev/null +++ b/unit/testing-utils/message.cpp @@ -0,0 +1,14 @@ +/*******************************************************************\ + + Module: Unit test utilities + + Author: Diffblue Ltd. + +\*******************************************************************/ + +/// \file +/// Global instance of `null_message_handlert`. + +#include "message.h" + +null_message_handlert null_message_handler; diff --git a/unit/testing-utils/message.h b/unit/testing-utils/message.h new file mode 100644 index 00000000000..4dfcfbd0aeb --- /dev/null +++ b/unit/testing-utils/message.h @@ -0,0 +1,16 @@ +/*******************************************************************\ + + Module: Unit test utilities + + Author: DiffBlue Limited. All rights reserved. + +\*******************************************************************/ + +#ifndef CPROVER_TESTING_UTILS_MESSAGE_H +#define CPROVER_TESTING_UTILS_MESSAGE_H + +#include + +extern null_message_handlert null_message_handler; + +#endif // CPROVER_TESTING_UTILS_MESSAGE_H