Remove unnecessary config.h includes

tautschnig · tautschnig · commit 74fbfba3bb0a · 2021-04-03T20:59:48.000Z
These files do not use configt (or its instantiation as config).
diff --git a/jbmc/src/java_bytecode/java_bytecode_typecheck.cpp b/jbmc/src/java_bytecode/java_bytecode_typecheck.cpp
@@ -13,7 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/std_types.h>
 #include <util/prefix.h>
-#include <util/config.h>
 
 #include "expr2java.h"
 
diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp b/jbmc/unit/java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp
@@ -11,7 +11,6 @@ Author: Diffblue Ltd.
 #include <istream>
 #include <memory>
 
-#include <util/config.h>
 #include <util/message.h>
 
 #include <java_bytecode/java_bytecode_language.h>
diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_initalizers.cpp b/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_initalizers.cpp
@@ -10,7 +10,6 @@ Author: Diffblue Limited.
 
 #include <memory>
 
-#include <util/config.h>
 #include <util/symbol_table.h>
 
 #include <java_bytecode/java_bytecode_language.h>
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_lambdas/java_bytecode_parse_lambda_method_table.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_lambdas/java_bytecode_parse_lambda_method_table.cpp
@@ -8,7 +8,6 @@ Author: Diffblue Ltd.
 
 #include <algorithm>
 #include <functional>
-#include <util/config.h>
 
 #include <java-testing-utils/require_parse_tree.h>
 
diff --git a/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp b/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp
@@ -20,7 +20,6 @@ Author: Diffblue Ltd.
 #include <java_bytecode/remove_instanceof.h>
 #include <java_bytecode/replace_java_nondet.h>
 
-#include <util/config.h>
 #include <util/options.h>
 
 #include <goto-instrument/cover.h>
diff --git a/scripts/expected_doxygen_warnings.txt b/scripts/expected_doxygen_warnings.txt
@@ -22,8 +22,8 @@ warning: Include graph for 'goto_instrument_parse_options.cpp' not generated, to
 warning: Included by graph for 'goto_functions.h' not generated, too many nodes (66), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'goto_model.h' not generated, too many nodes (111), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'arith_tools.h' not generated, too many nodes (183), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'c_types.h' not generated, too many nodes (142), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'config.h' not generated, too many nodes (88), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'c_types.h' not generated, too many nodes (143), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'config.h' not generated, too many nodes (78), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'exception_utils.h' not generated, too many nodes (61), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'expr.h' not generated, too many nodes (87), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'expr_util.h' not generated, too many nodes (61), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
diff --git a/src/ansi-c/gcc_types.cpp b/src/ansi-c/gcc_types.cpp
@@ -8,8 +8,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "gcc_types.h"
 
-#include <util/config.h>
 #include <util/c_types.h>
+#include <util/ieee_float.h>
 
 floatbv_typet gcc_float16_type()
 {
diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h
@@ -15,7 +15,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <ansi-c/ansi_c_language.h>
 #include <ansi-c/c_object_factory_parameters.h>
 
-#include <util/config.h>
 #include <util/parse_options.h>
 #include <util/timestamper.h>
 #include <util/ui_message.h>
diff --git a/src/goto-analyzer/goto_analyzer_parse_options.h b/src/goto-analyzer/goto_analyzer_parse_options.h
@@ -89,7 +89,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H
 #define CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H
 
-#include <util/config.h>
 #include <util/parse_options.h>
 #include <util/timestamper.h>
 #include <util/ui_message.h>
diff --git a/src/goto-instrument/accelerate/util.cpp b/src/goto-instrument/accelerate/util.cpp
@@ -14,17 +14,17 @@ Author: Matt Lewis
 #include <iostream>
 #include <algorithm>
 
+#include <util/c_types.h>
 #include <util/std_types.h>
-#include <util/config.h>
 
 signedbv_typet signed_poly_type()
 {
-  return signedbv_typet(config.ansi_c.int_width);
+  return signed_int_type();
 }
 
 unsignedbv_typet unsigned_poly_type()
 {
-  return unsignedbv_typet(config.ansi_c.int_width);
+  return unsigned_int_type();
 }
 
 /**
diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp
@@ -13,7 +13,6 @@ Date: May 2016
 
 #include "cover.h"
 
-#include <util/config.h>
 #include <util/message.h>
 #include <util/make_unique.h>
 #include <util/cmdline.h>
diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp
@@ -15,9 +15,9 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/arith_tools.h>
 #include <util/c_types.h>
-#include <util/config.h>
 #include <util/expr_util.h>
 #include <util/find_symbols.h>
+#include <util/ieee_float.h>
 #include <util/pointer_expr.h>
 #include <util/prefix.h>
 #include <util/simplify_expr.h>
diff --git a/src/goto-programs/json_goto_trace.cpp b/src/goto-programs/json_goto_trace.cpp
@@ -15,7 +15,6 @@ Author: Daniel Kroening
 
 #include <langapi/language_util.h>
 #include <util/arith_tools.h>
-#include <util/config.h>
 #include <util/invariant.h>
 #include <util/simplify_expr.h>
 
diff --git a/src/linking/static_lifetime_init.cpp b/src/linking/static_lifetime_init.cpp
@@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/arith_tools.h>
 #include <util/c_types.h>
-#include <util/config.h>
 #include <util/expr_initializer.h>
 #include <util/namespace.h>
 #include <util/prefix.h>
diff --git a/src/memory-analyzer/analyze_symbol.cpp b/src/memory-analyzer/analyze_symbol.cpp
@@ -13,7 +13,6 @@ Author: Malte Mues <mail.mues@gmail.com>
 
 #include <util/c_types.h>
 #include <util/c_types_util.h>
-#include <util/config.h>
 #include <util/expr_initializer.h>
 #include <util/pointer_expr.h>
 #include <util/pointer_offset_size.h>
diff --git a/unit/json_symbol_table.cpp b/unit/json_symbol_table.cpp
@@ -18,7 +18,6 @@
 #include <langapi/mode.h>
 
 #include <util/cmdline.h>
-#include <util/config.h>
 #include <util/message.h>
 #include <util/options.h>
 #include <util/symbol_table.h>

Original file line number	Diff line number	Diff line change
`@@ -8,8 +8,8 @@ Author: Daniel Kroening, [email protected]`
`8`	`8`
`9`	`9`	`#include "gcc_types.h"`
`10`	`10`
`11`		`-#include <util/config.h>`
`12`	`11`	`#include <util/c_types.h>`
	`12`	`+#include <util/ieee_float.h>`
`13`	`13`
`14`	`14`	`floatbv_typet gcc_float16_type()`
`15`	`15`	`{`
Original file line number	Diff line number	Diff line change
`@@ -14,17 +14,17 @@ Author: Matt Lewis`
`14`	`14`	`#include <iostream>`
`15`	`15`	`#include <algorithm>`
`16`	`16`
	`17`	`+#include <util/c_types.h>`
`17`	`18`	`#include <util/std_types.h>`
`18`		`-#include <util/config.h>`
`19`	`19`
`20`	`20`	`signedbv_typet signed_poly_type()`
`21`	`21`	`{`
`22`		`- return signedbv_typet(config.ansi_c.int_width);`
	`22`	`+ return signed_int_type();`
`23`	`23`	`}`
`24`	`24`
`25`	`25`	`unsignedbv_typet unsigned_poly_type()`
`26`	`26`	`{`
`27`		`- return unsignedbv_typet(config.ansi_c.int_width);`
	`27`	`+ return unsigned_int_type();`
`28`	`28`	`}`
`29`	`29`
`30`	`30`	`/**`