Merge pull request #6060 from tautschnig/includes-cleanup

Remove unnecessary includes

Author: tautschnig

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