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.

This is a second iteration of this cleanup; the first round took place in
450845d.

Author: tautschnig

jbmc/src/java_bytecode/code_with_references.cpp

@@ -9,8 +9,6 @@ Author: Romain Brenguier, [email protected]
 #include "code_with_references.h"
 #include "java_types.h"
 
-#include <goto-programs/goto_instruction_code.h>
-
 #include <util/arith_tools.h>
 
 codet allocate_array(

jbmc/src/java_bytecode/java_bytecode_internal_additions.cpp

@@ -13,7 +13,6 @@ Author: Daniel Kroening, [email protected]
 #include "remove_exceptions.h"
 
 #include <util/c_types.h>
-#include <util/cprover_prefix.h>
 #include <util/pointer_expr.h>
 #include <util/std_types.h>
 #include <util/symbol_table_base.h>

jbmc/src/java_bytecode/java_bytecode_parser.cpp

@@ -18,7 +18,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/parser.h>
 #include <util/std_expr.h>
 #include <util/string_constant.h>
-#include <util/optional.h>
 
 #include "bytecode_info.h"
 #include "java_bytecode_parse_tree.h"

jbmc/src/java_bytecode/java_bytecode_typecheck_expr.cpp

@@ -11,7 +11,6 @@ Author: Daniel Kroening, [email protected]
 
 #include "java_bytecode_typecheck.h"
 
-#include <util/cprover_prefix.h>
 #include <util/pointer_expr.h>
 #include <util/prefix.h>
 #include <util/std_code.h>

jbmc/src/java_bytecode/java_local_variable_table.cpp

@@ -16,7 +16,7 @@ Author: Chris Smowton, [email protected]
 #include <util/arith_tools.h>
 #include <util/invariant.h>
 #include <util/string2int.h>
-#include <util/symbol_table.h>
+#include <util/symbol_table_base.h>
 
 #include <iostream>
 

jbmc/src/java_bytecode/lambda_synthesis.cpp

@@ -11,7 +11,6 @@ Author: Diffblue Ltd.
 
 #include "lambda_synthesis.h"
 
-#include "jar_file.h"
 #include "java_bytecode_convert_method.h"
 #include "java_bytecode_parse_tree.h"
 #include "java_static_initializers.h"

jbmc/src/java_bytecode/lazy_goto_model.cpp

@@ -8,7 +8,6 @@
 #include <util/config.h>
 #include <util/exception_utils.h>
 #include <util/journalling_symbol_table.h>
-#include <util/options.h>
 
 #include <goto-programs/initialize_goto_model.h>
 #include <goto-programs/read_goto_binary.h>

jbmc/src/java_bytecode/mz_zip_archive.cpp

@@ -9,7 +9,6 @@ Author: Diffblue Ltd
 #include "mz_zip_archive.h"
 #include <stdexcept>
 #include <string>
-#include <algorithm>
 #define _LARGEFILE64_SOURCE 1
 #include <miniz/miniz.h>
 

jbmc/src/java_bytecode/remove_exceptions.cpp

@@ -18,8 +18,6 @@ Date:   December 2016
 #include <iostream>
 #endif
 
-#include <algorithm>
-
 #include <util/c_types.h>
 #include <util/pointer_expr.h>
 #include <util/std_code.h>

jbmc/unit/java-testing-utils/require_goto_statements.h

@@ -11,8 +11,6 @@ Author: Diffblue Ltd.
 
 #include <goto-programs/goto_instruction_code.h>
 
-#include <util/optional.h>
-
 #include <regex>
 
 class symbol_tablet;

jbmc/unit/java-testing-utils/require_type.h

@@ -15,7 +15,6 @@ Author: Diffblue Ltd.
 #ifndef CPROVER_JAVA_TESTING_UTILS_REQUIRE_TYPE_H
 #define CPROVER_JAVA_TESTING_UTILS_REQUIRE_TYPE_H
 
-#include <util/optional.h>
 #include <util/std_types.h>
 #include <java_bytecode/java_types.h>
 

jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_initalizers.cpp

@@ -12,8 +12,6 @@ Author: Diffblue Limited.
 
 #include <util/symbol_table.h>
 
-#include <java_bytecode/java_bytecode_language.h>
-
 #include <java-testing-utils/load_java_class.h>
 #include <java-testing-utils/require_type.h>
 

src/analyses/ai.cpp

@@ -16,7 +16,6 @@ Author: Daniel Kroening, [email protected]
 #include <type_traits>
 
 #include <util/invariant.h>
-#include <util/std_code.h>
 
 void ai_baset::output(
   const namespacet &ns,

src/analyses/constant_propagator.cpp

@@ -29,7 +29,6 @@ Author: Peter Schrammel
 
 #include <langapi/language_util.h>
 
-#include <algorithm>
 #include <array>
 
 /// Assign value `rhs` to `lhs`, recording any newly-known constants in

src/analyses/does_remove_const.cpp

@@ -14,7 +14,6 @@ Author: Diffblue Ltd.
 #include <goto-programs/goto_program.h>
 
 #include <util/pointer_expr.h>
-#include <util/std_code.h>
 
 /// A naive analysis to look for casts that remove const-ness from pointers.
 /// \param goto_program: the goto program to check

src/analyses/goto_rw.cpp

@@ -21,7 +21,6 @@ Date: April 2010
 #include <util/pointer_expr.h>
 #include <util/pointer_offset_size.h>
 #include <util/simplify_expr.h>
-#include <util/std_code.h>
 
 #include <langapi/language_util.h>
 

src/analyses/guard_bdd.cpp

@@ -11,8 +11,6 @@ Author: Romain Brenguier, [email protected]
 
 #include "guard_bdd.h"
 
-#include <algorithm>
-
 #include <solvers/prop/bdd_expr.h>
 #include <util/expr_util.h>
 #include <util/invariant.h>

src/analyses/guard_expr.cpp

@@ -13,7 +13,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/expr_util.h>
 #include <util/invariant.h>
-#include <util/simplify_utils.h>
 #include <util/std_expr.h>
 
 exprt guard_exprt::guard_expr(exprt expr) const

src/analyses/local_bitvector_analysis.cpp

@@ -15,7 +15,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/pointer_expr.h>
 #include <util/std_code.h>
-#include <util/symbol_table.h>
+#include <util/symbol.h>
 
 void local_bitvector_analysist::flagst::print(std::ostream &out) const
 {

src/analyses/local_safe_pointers.cpp

@@ -14,7 +14,6 @@ Author: Diffblue Ltd
 #include <util/expr_iterator.h>
 #include <util/expr_util.h>
 #include <util/format_expr.h>
-#include <util/symbol_table.h>
 
 /// Return structure for `get_null_checked_expr` and
 /// `get_conditional_checked_expr`

src/analyses/static_analysis.cpp

@@ -16,7 +16,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/expr_util.h>
 #include <util/pointer_expr.h>
-#include <util/std_code.h>
 
 #include "is_threaded.h"
 

src/analyses/uncaught_exceptions_analysis.cpp

@@ -16,7 +16,7 @@ Author: Cristina David
 
 #include <util/namespace.h>
 #include <util/pointer_expr.h>
-#include <util/symbol_table.h>
+#include <util/symbol_table_base.h>
 
 #include <goto-programs/goto_functions.h>
 

src/analyses/variable-sensitivity/abstract_environment.cpp

@@ -7,12 +7,10 @@
 \*******************************************************************/
 
 #include <analyses/variable-sensitivity/abstract_environment.h>
-#include <analyses/variable-sensitivity/abstract_object_statistics.h>
 #include <analyses/variable-sensitivity/variable_sensitivity_object_factory.h>
 
 #include <util/expr_util.h>
 #include <util/simplify_expr.h>
-#include <util/simplify_expr_class.h>
 #include <util/simplify_utils.h>
 #include <util/symbol_table.h>
 

src/analyses/variable-sensitivity/variable_sensitivity_configuration.cpp

@@ -11,6 +11,8 @@
 #include "variable_sensitivity_configuration.h"
 
 #include <limits>
+
+#include <util/exception_utils.h>
 #include <util/options.h>
 
 static void check_one_of_options(

src/analyses/variable-sensitivity/variable_sensitivity_configuration.h

@@ -12,8 +12,7 @@
 #define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VARIABLE_SENSITIVITY_CONFIGURATION_H
 
 #include <map>
-
-#include <util/exception_utils.h>
+#include <string>
 
 class optionst;
 

src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp

@@ -12,7 +12,7 @@ Date: April 2016
 
 #include <util/cprover_prefix.h>
 #include <util/pointer_expr.h>
-#include <util/symbol_table.h>
+#include <util/symbol_table_base.h>
 
 #include <algorithm>
 

src/ansi-c/ansi_c_convert_type.cpp

@@ -13,7 +13,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/c_types.h>
 #include <util/config.h>
-#include <util/std_code.h>
 #include <util/std_types.h>
 #include <util/string_constant.h>
 

src/ansi-c/c_typecheck_code.cpp

@@ -11,7 +11,6 @@ Author: Daniel Kroening, [email protected]
 
 #include "c_typecheck_base.h"
 
-#include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/config.h>
 #include <util/expr_util.h>

src/ansi-c/c_typecheck_type.cpp

@@ -13,8 +13,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <unordered_set>
 
-#include <goto-programs/goto_instruction_code.h>
-
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/config.h>

src/ansi-c/goto_check_c.cpp

@@ -42,7 +42,6 @@ Author: Daniel Kroening, [email protected]
 #include <langapi/mode.h>
 
 #include <algorithm>
-#include <optional>
 
 class goto_check_ct
 {

src/cpp/cpp_typecheck.cpp

@@ -11,8 +11,6 @@ Author: Daniel Kroening, [email protected]
 
 #include "cpp_typecheck.h"
 
-#include <algorithm>
-
 #include <util/pointer_expr.h>
 #include <util/source_location.h>
 #include <util/symbol.h>

src/cpp/cpp_typecheck_destructor.cpp

@@ -11,8 +11,6 @@ Author: Daniel Kroening, [email protected]
 
 #include "cpp_typecheck.h"
 
-#include <goto-programs/goto_instruction_code.h>
-
 #include <util/pointer_expr.h>
 
 bool cpp_typecheckt::find_dtor(const symbolt &symbol) const

src/cpp/cpp_typecheck_initializer.cpp

@@ -11,8 +11,6 @@ Author: Daniel Kroening, [email protected]
 
 #include "cpp_typecheck.h"
 
-#include <goto-programs/goto_instruction_code.h>
-
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/expr_initializer.h>

src/cpp/template_map.cpp

@@ -11,8 +11,8 @@ Author: Daniel Kroening, [email protected]
 
 #include "template_map.h"
 
-#include <util/c_types.h>
 #include <util/invariant.h>
+#include <util/pointer_expr.h>
 #include <util/std_expr.h>
 
 #include "cpp_template_parameter.h"

src/cprover/axioms.cpp

@@ -12,14 +12,12 @@ Author: Daniel Kroening, [email protected]
 #include "axioms.h"
 
 #include <util/arith_tools.h>
-#include <util/bitvector_expr.h>
 #include <util/c_types.h>
 #include <util/format_expr.h>
 #include <util/namespace.h>
 #include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
 #include <util/prefix.h>
-#include <util/simplify_expr.h>
 #include <util/string_constant.h>
 #include <util/symbol.h>
 

src/cprover/c_safety_checks.cpp

@@ -13,7 +13,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/arith_tools.h>
 #include <util/c_types.h>
-#include <util/options.h>
 #include <util/pointer_expr.h>
 #include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>

src/cprover/console.cpp

@@ -16,13 +16,13 @@ Author: Daniel Kroening, [email protected]
 #  include <io.h>
 #  include <windows.h>
 #  define isatty _isatty
+#include <util/unicode.h>
 #else
 #  include <unistd.h>
 #endif
 
 #include <util/run.h>
 #include <util/string_utils.h>
-#include <util/unicode.h>
 
 #ifdef _WIN32
 class windows_coutt : public std::streambuf

src/cprover/cprover_main.cpp

@@ -9,11 +9,11 @@ Author: Daniel Kroening, [email protected]
 /// \file
 /// cprover Main Module
 
-#include <util/unicode.h>
-
 #include "cprover_parse_options.h"
 
 #ifdef _MSC_VER
+#include <util/unicode.h>
+
 #  include <windows.h>
 #endif
 

src/cprover/cprover_parse_options.cpp

@@ -26,7 +26,6 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/loop_ids.h>
 #include <goto-programs/remove_function_pointers.h>
 #include <goto-programs/set_properties.h>
-#include <goto-programs/show_goto_functions.h>
 #include <goto-programs/show_properties.h>
 
 #include <ansi-c/ansi_c_language.h>

src/cprover/find_variables.cpp

@@ -13,8 +13,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/pointer_expr.h>
 
-#include "state.h"
-
 static void find_variables_rec(
   const exprt &src,
   std::unordered_set<symbol_exprt, irep_hash> &result)

src/cprover/instrument_contracts.cpp

@@ -12,7 +12,6 @@ Author: Daniel Kroening, [email protected]
 #include "instrument_contracts.h"
 
 #include <util/c_types.h>
-#include <util/format_expr.h>
 #include <util/mathematical_expr.h>
 #include <util/pointer_predicates.h>
 #include <util/prefix.h>

src/cprover/may_alias.cpp

@@ -12,16 +12,12 @@ Author: Daniel Kroening, [email protected]
 #include "may_alias.h"
 
 #include <util/c_types.h>
-#include <util/format_expr.h>
-#include <util/format_type.h>
 #include <util/namespace.h>
 #include <util/pointer_expr.h>
 #include <util/prefix.h>
 #include <util/std_expr.h>
 #include <util/symbol.h>
 
-#include <iostream>
-
 bool permitted_by_strict_aliasing(const typet &a, const typet &b)
 {
   // C99; ISO/IEC 9899:1999 6.5/7