diffblue · tautschnig · Jun 5, 2018 · May 23, 2018 · May 23, 2018 · May 24, 2018
diff --git 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 <testing-utils/free_form_cmdline.h>
-#include <testing-utils/catch.hpp>
 #include <iostream>
+#include <testing-utils/catch.hpp>
+#include <testing-utils/free_form_cmdline.h>
+#include <testing-utils/message.h>
 
 #include <util/config.h>
 #include <util/suffix.h>
@@ -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/...nit/java_bytecode/java_bytecode_parse_lambdas/java_bytecode_parse_lambda_method_table.cpp b/...nit/java_bytecode/java_bytecode_parse_lambdas/java_bytecode_parse_lambda_method_table.cpp
@@ -8,13 +8,13 @@
 
 #include <algorithm>
 #include <functional>
-#include <util/message.h>
 #include <util/config.h>
 
 #include <java-testing-utils/require_parse_tree.h>
 
-#include <testing-utils/catch.hpp>
 #include <java_bytecode/java_bytecode_parser.h>
+#include <testing-utils/catch.hpp>
+#include <testing-utils/message.h>
 
 #include <java_bytecode/java_bytecode_parse_tree.h>
 #include <java_bytecode/java_types.h>
@@ -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<java_bytecode_parse_treet> 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<java_bytecode_parse_treet> 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,15 +646,14 @@ 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.")
       {
         optionalt<java_bytecode_parse_treet> 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<java_bytecode_parse_treet> 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
@@ -7,8 +7,9 @@
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
 #include <java-testing-utils/load_java_class.h>
+#include <testing-utils/catch.hpp>
+#include <testing-utils/message.h>
 
 #include <goto-programs/goto_convert_functions.h>
 #include <goto-programs/remove_virtual_functions.h>
@@ -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
@@ -6,8 +6,9 @@
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
 #include <java-testing-utils/load_java_class.h>
+#include <testing-utils/catch.hpp>
+#include <testing-utils/message.h>
 
 #include <goto-programs/goto_convert_functions.h>
 #include <goto-programs/remove_virtual_functions.h>
@@ -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
@@ -7,6 +7,7 @@ Author: Chris Smowton, chris@smowton.net
 \*******************************************************************/
 
 #include <testing-utils/catch.hpp>
+#include <testing-utils/message.h>
 
 #include <goto-programs/goto_inline.h>
 #include <goto-programs/initialize_goto_model.h>
@@ -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
@@ -8,10 +8,10 @@
 
 #include <json/json_parser.h>
 #include <testing-utils/catch.hpp>
+#include <testing-utils/message.h>
 
 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
@@ -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
@@ -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
@@ -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 <util/message.h>
+
+extern null_message_handlert null_message_handler;
+
+#endif // CPROVER_TESTING_UTILS_MESSAGE_H