Remove unnecessary includes

Manual removal of includes based on include-what-you-use's output,
filtered for includes that should be removed. The goal is to avoid
unnecessary build dependencies, reducing the amount of code that needs
to be rebuilt during incremental builds. The build time for fresh
rebuilds decreases by about 7% as the following experiment shows:

```
rm -rf build && ccache -C
cmake -H. -Bbuild -G Ninja \
  -DCMAKE_BUILD_TYPE=Release \
  -DCMAKE_EXE_LINKER_FLAGS="-fuse-ld=lld -Wl,--threads"
/usr/bin/time -v ninja -C build -j32
```

Repeated execution for both develop and this branch producing the
following data, which less than 1s of variation across multiple runs:

develop:
```
  Command being timed: "ninja -C build -j32"
  User time (seconds): 2714.02
  System time (seconds): 203.75
  Percent of CPU this job got: 2833%
  Elapsed (wall clock) time (h:mm:ss or m:ss): 1:42.96
```

this PR:
```
  Command being timed: "ninja -C build -j32"
  User time (seconds): 2507.14
  System time (seconds): 189.95
  Percent of CPU this job got: 2822%
  Elapsed (wall clock) time (h:mm:ss or m:ss): 1:35.56
```

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