Remove unnecessary includes

jbmc/src/janalyzer/janalyzer_main.cpp

@@ -11,7 +11,9 @@ Author: Peter Schrammel
 
 #include "janalyzer_parse_options.h"
 
-#include <util/unicode.h>
+#ifdef _MSC_VER
+#  include <util/unicode.h>
+#endif
 
 #ifdef _MSC_VER
 int wmain(int argc, const wchar_t **argv_wide)

jbmc/src/janalyzer/janalyzer_parse_options.cpp

@@ -19,14 +19,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <ansi-c/ansi_c_language.h>
 
-#include <goto-programs/goto_convert_functions.h>
-#include <goto-programs/goto_inline.h>
-#include <goto-programs/read_goto_binary.h>
-#include <goto-programs/remove_complex.h>
-#include <goto-programs/remove_function_pointers.h>
 #include <goto-programs/remove_returns.h>
 #include <goto-programs/remove_skip.h>
-#include <goto-programs/remove_vector.h>
 #include <goto-programs/remove_virtual_functions.h>
 #include <goto-programs/set_properties.h>
 #include <goto-programs/show_properties.h>
@@ -36,7 +30,6 @@ Author: Daniel Kroening, [email protected]
 #include <analyses/dependence_graph.h>
 #include <analyses/goto_check.h>
 #include <analyses/interval_domain.h>
-#include <analyses/is_threaded.h>
 #include <analyses/local_may_alias.h>
 
 #include <java_bytecode/java_bytecode_language.h>
@@ -52,7 +45,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/config.h>
 #include <util/exit_codes.h>
 #include <util/options.h>
-#include <util/unicode.h>
 #include <util/version.h>
 
 #include <goto-analyzer/static_show_domain.h>

jbmc/src/janalyzer/janalyzer_parse_options.h

@@ -102,21 +102,19 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/parse_options.h>
 #include <util/timestamper.h>
-#include <util/ui_message.h>
 
 #include <langapi/language.h>
 
-#include <goto-programs/goto_model.h>
 #include <goto-programs/show_goto_functions.h>
 #include <goto-programs/show_properties.h>
 
-#include <analyses/ai.h>
 #include <analyses/goto_check.h>
 
 #include <java_bytecode/java_bytecode_language.h>
 
-class bmct;
-class goto_functionst;
+class abstract_goto_modelt;
+class ai_baset;
+class goto_model_functiont;
 class optionst;
 
 // clang-format off

jbmc/src/java_bytecode/assignments_from_json.cpp

@@ -11,15 +11,19 @@ Author: Diffblue Ltd.
 #include "ci_lazy_methods_needed.h"
 #include "code_with_references.h"
 #include "java_static_initializers.h"
-#include "java_string_library_preprocess.h"
 #include "java_string_literals.h"
+#include "java_types.h"
 #include "java_utils.h"
 
 #include <goto-programs/class_identifier.h>
+
 #include <util/allocate_objects.h>
+#include <util/arith_tools.h>
 #include <util/array_element_from_pointer.h>
 #include <util/expr_initializer.h>
-#include <util/prefix.h>
+#include <util/ieee_float.h>
+#include <util/json.h>
+#include <util/symbol_table_base.h>
 #include <util/unicode.h>
 
 /// Values passed around between most functions of the recursive deterministic

jbmc/src/java_bytecode/assignments_from_json.h

@@ -12,7 +12,6 @@ Author: Diffblue Ltd.
 #define CPROVER_JAVA_BYTECODE_ASSIGNMENTS_FROM_JSON_H
 
 #include "code_with_references.h"
-#include <util/std_code.h>
 
 class jsont;
 class symbol_table_baset;

jbmc/src/java_bytecode/ci_lazy_methods.cpp

@@ -7,13 +7,13 @@ Author: Diffblue Ltd.
 \*******************************************************************/
 
 #include "ci_lazy_methods.h"
-#include "java_entry_point.h"
+#include "java_bytecode_language.h"
 #include "java_class_loader.h"
-#include "java_utils.h"
-#include "java_string_library_preprocess.h"
+#include "java_entry_point.h"
 #include "remove_exceptions.h"
 
 #include <util/expr_iterator.h>
+#include <util/namespace.h>
 #include <util/suffix.h>
 
 #include <goto-programs/resolve_inherited_component.h>

jbmc/src/java_bytecode/ci_lazy_methods.h

@@ -12,22 +12,21 @@ Author: Diffblue Ltd.
 #ifndef CPROVER_JAVA_BYTECODE_GATHER_METHODS_LAZILY_H
 #define CPROVER_JAVA_BYTECODE_GATHER_METHODS_LAZILY_H
 
-#include "ci_lazy_methods_needed.h"
 #include "java_bytecode_parse_tree.h"
-#include "java_class_loader.h"
-#include "select_pointer_type.h"
 #include "synthetic_methods_map.h"
 
-#include <map>
 #include <functional>
+#include <map>
+#include <unordered_set>
 
 #include <util/irep.h>
-#include <util/symbol_table.h>
-#include <util/message.h>
 
 #include <goto-programs/class_hierarchy.h>
 
-class java_string_library_preprocesst;
+class ci_lazy_methods_neededt;
+class java_class_loadert;
+class message_handlert;
+class select_pointer_typet;
 
 // Map from method id to class_method_and_bytecodet
 class method_bytecodet

jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp

@@ -15,10 +15,11 @@ Author: Chris Smowton, [email protected]
 
 #include <util/namespace.h>
 #include <util/std_types.h>
+#include <util/symbol_table.h>
 
-#include <string>
-
+#include "generic_parameter_specialization_map.h"
 #include "java_static_initializers.h"
+#include "java_types.h"
 #include "select_pointer_type.h"
 
 /// Notes `method_symbol_name` is referenced from some reachable function, and

jbmc/src/java_bytecode/ci_lazy_methods_needed.h

@@ -12,14 +12,15 @@ Author: Chris Smowton, [email protected]
 #ifndef CPROVER_JAVA_BYTECODE_CI_LAZY_METHODS_H
 #define CPROVER_JAVA_BYTECODE_CI_LAZY_METHODS_H
 
-#include <set>
 #include <unordered_set>
-#include <util/namespace.h>
-#include <util/symbol_table.h>
-#include <vector>
 
-class select_pointer_typet;
+#include <util/irep.h>
+
+class namespacet;
 class pointer_typet;
+class select_pointer_typet;
+class symbol_tablet;
+class typet;
 
 class ci_lazy_methods_neededt
 {

jbmc/src/java_bytecode/convert_java_nondet.cpp

@@ -15,11 +15,8 @@ Author: Reuben Thomas, [email protected]
 #include <goto-programs/goto_model.h>
 #include <goto-programs/remove_skip.h>
 
-#include <util/irep_ids.h>
-
-#include <memory>
-
 #include "java_object_factory.h" // gen_nondet_init
+#include "java_object_factory_parameters.h"
 #include "java_utils.h"
 
 /// Returns true if `expr` is a nondet pointer that isn't a function pointer or

jbmc/src/java_bytecode/convert_java_nondet.h

@@ -12,7 +12,6 @@ Author: Reuben Thomas, [email protected]
 #ifndef CPROVER_JAVA_BYTECODE_CONVERT_NONDET_H
 #define CPROVER_JAVA_BYTECODE_CONVERT_NONDET_H
 
-#include <cstddef> // size_t
 #include <util/irep.h>
 
 class goto_functionst;

jbmc/src/java_bytecode/create_array_with_type_intrinsic.cpp

@@ -11,8 +11,6 @@ Author: Diffblue Ltd.
 
 #include "create_array_with_type_intrinsic.h"
 
-#include <goto-programs/class_identifier.h>
-
 #include <java_bytecode/java_types.h>
 
 #include <util/fresh_symbol.h>

jbmc/src/java_bytecode/create_array_with_type_intrinsic.h

@@ -12,9 +12,10 @@ Author: Diffblue Ltd.
 #ifndef CPROVER_JAVA_BYTECODE_CREATE_ARRAY_WITH_TYPE_INTRINSIC_H
 #define CPROVER_JAVA_BYTECODE_CREATE_ARRAY_WITH_TYPE_INTRINSIC_H
 
-#include <util/message.h>
 #include <util/std_code.h>
-#include <util/symbol_table_base.h>
+
+class message_handlert;
+class symbol_table_baset;
 
 irep_idt get_create_array_with_type_name();
 

jbmc/src/java_bytecode/expr2java.cpp

@@ -8,12 +8,8 @@ Author: Daniel Kroening, [email protected]
 
 #include "expr2java.h"
 
-#include <sstream>
-
 #include <util/namespace.h>
-#include <util/std_types.h>
 #include <util/std_expr.h>
-#include <util/symbol.h>
 #include <util/unicode.h>
 #include <util/arith_tools.h>
 #include <util/ieee_float.h>

jbmc/src/java_bytecode/expr2java.h

@@ -11,8 +11,6 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_JAVA_BYTECODE_EXPR2JAVA_H
 
 #include <cmath>
-#include <limits>
-#include <numeric>
 #include <sstream>
 #include <string>
 

jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.cpp

@@ -2,8 +2,6 @@
 
 #include "generic_parameter_specialization_map_keys.h"
 
-#include <util/range.h>
-
 /// Add the parameters and their types for each generic parameter of the
 /// given generic pointer type to the map.
 /// Own the keys and pop from their stack on destruction.

jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.h

@@ -3,8 +3,7 @@
 #ifndef CPROVER_JAVA_BYTECODE_GENERIC_PARAMETER_SPECIALIZATION_MAP_KEYS_H
 #define CPROVER_JAVA_BYTECODE_GENERIC_PARAMETER_SPECIALIZATION_MAP_KEYS_H
 
-#include "select_pointer_type.h"
-#include "java_types.h"
+#include "generic_parameter_specialization_map.h"
 
 /// \file
 /// Generic-parameter-specialization-map entries owner class.

jbmc/src/java_bytecode/jar_file.cpp

@@ -10,11 +10,7 @@ Author: Diffblue Ltd
 
 #include <algorithm>
 #include <cctype>
-
-#include <util/invariant.h>
-#include <util/suffix.h>
-
-#include "java_class_loader_limit.h"
+#include <sstream>
 
 void jar_filet::initialize_file_index()
 {

jbmc/src/java_bytecode/jar_file.h

@@ -10,7 +10,6 @@ Author: Diffblue Ltd
 #define CPROVER_JAVA_BYTECODE_JAR_FILE_H
 
 #include <unordered_map>
-#include <memory>
 #include <string>
 #include <vector>
 

jbmc/src/java_bytecode/jar_pool.h

@@ -12,7 +12,7 @@ Author: Daniel Kroening, [email protected]
 #include <map>
 #include <string>
 
-class jar_filet;
+#include "jar_file.h"
 
 /// A chache for jar_filet objects, by file name
 class jar_poolt

jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp

@@ -11,11 +11,13 @@ Author: Kurt Degiogrio, [email protected]
 #include "java_types.h"
 #include "java_utils.h"
 
+#include <util/arith_tools.h>
+#include <util/cprover_prefix.h>
 #include <util/expr_iterator.h>
+#include <util/message.h>
 #include <util/namespace.h>
-#include <util/cprover_prefix.h>
 #include <util/std_types.h>
-#include <util/arith_tools.h>
+#include <util/symbol_table.h>
 
 // Disable linter to allow an std::string constant.
 const std::string next_thread_id = CPROVER_PREFIX "_next_thread_id";// NOLINT(*)

jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.h

@@ -8,8 +8,8 @@ Author: Kurt Degiogrio, [email protected]
 #ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONCURRENCY_INSTRUMENTATION_H
 #define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONCURRENCY_INSTRUMENTATION_H
 
-#include <util/symbol_table.h>
-#include <util/message.h>
+class message_handlert;
+class symbol_tablet;
 
 void convert_threadblock(symbol_tablet &symbol_table);
 void convert_synchronized_methods(

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -15,21 +15,17 @@ Author: Daniel Kroening, [email protected]
 #include <iostream>
 #endif
 
+#include "ci_lazy_methods.h"
+#include "java_bytecode_convert_method.h"
 #include "java_root_class.h"
 #include "java_types.h"
-#include "java_bytecode_convert_method.h"
-#include "java_bytecode_language.h"
 #include "java_utils.h"
 
-#include <goto-programs/class_identifier.h>
-
 #include <util/arith_tools.h>
-#include <util/c_types.h>
 #include <util/expr_initializer.h>
 #include <util/namespace.h>
 #include <util/prefix.h>
 #include <util/std_expr.h>
-#include <util/suffix.h>
 
 class java_bytecode_convert_classt
 {

jbmc/src/java_bytecode/java_bytecode_convert_class.h

@@ -13,11 +13,13 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_CLASS_H
 
 #include <unordered_set>
-#include <util/symbol_table.h>
-#include <util/message.h>
 
 #include "java_bytecode_parse_tree.h"
-#include "java_bytecode_language.h"
+#include "java_class_loader.h"
+
+class java_string_library_preprocesst;
+class method_bytecodet;
+class symbol_tablet;
 
 /// See class \ref java_bytecode_convert_classt
 bool java_bytecode_convert_class(

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -24,34 +24,26 @@ Author: Daniel Kroening, [email protected]
 #include "java_utils.h"
 #include "lambda_synthesis.h"
 #include "pattern.h"
-#include "remove_exceptions.h"
 
 #include <util/arith_tools.h>
+#include <util/bitvector_expr.h>
 #include <util/c_types.h>
 #include <util/expr_initializer.h>
 #include <util/floatbv_expr.h>
 #include <util/ieee_float.h>
 #include <util/invariant.h>
 #include <util/namespace.h>
 #include <util/prefix.h>
-#include <util/simplify_expr.h>
+#include <util/prefix_filter.h>
 #include <util/std_expr.h>
-#include <util/string2int.h>
 #include <util/threeval.h>
 
-#include <goto-programs/cfg.h>
-#include <goto-programs/class_hierarchy.h>
-#include <goto-programs/remove_returns.h>
 #include <goto-programs/resolve_inherited_component.h>
 
-#include <analyses/cfg_dominators.h>
 #include <analyses/uncaught_exceptions_analysis.h>
 
 #include <algorithm>
-#include <functional>
 #include <limits>
-#include <regex>
-#include <unordered_set>
 
 /// Iterates through the parameters of the function type \p ftype, finds a new
 /// new name for each parameter and renames them in `ftype.parameters()` as