move bitvector types to bitvector_types.h

The rationale is that types of a particular group (say bitvectors or
pointers) are often used together with the expressions that are specific for
them.

The goal is that std_types.h will only contain the basic types, such as
bool_typet.

Author: kroening

scripts/expected_doxygen_warnings.txt

@@ -82,7 +82,7 @@
 warning: Include graph for 'goto_instrument_parse_options.cpp' not generated, too many nodes (97), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 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 (110), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'arith_tools.h' not generated, too many nodes (181), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'arith_tools.h' not generated, too many nodes (182), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'c_types.h' not generated, too many nodes (110), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'config.h' not generated, too many nodes (87), 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.
@@ -96,6 +96,6 @@ warning: Included by graph for 'pointer_expr.h' not generated, too many nodes (1
 warning: Included by graph for 'prefix.h' not generated, too many nodes (86), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'simplify_expr.h' not generated, too many nodes (77), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'std_code.h' not generated, too many nodes (78), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'std_expr.h' not generated, too many nodes (243), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'std_types.h' not generated, too many nodes (117), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'std_expr.h' not generated, too many nodes (241), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'std_types.h' not generated, too many nodes (102), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'symbol_table.h' not generated, too many nodes (95), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.

src/analyses/variable-sensitivity/abstract_value_object.cpp

@@ -12,8 +12,11 @@
 #include <analyses/variable-sensitivity/context_abstract_object.h>
 #include <analyses/variable-sensitivity/interval_abstract_value.h>
 #include <analyses/variable-sensitivity/value_set_abstract_object.h>
+
 #include <goto-programs/adjust_float_expressions.h>
+
 #include <util/arith_tools.h>
+#include <util/bitvector_types.h>
 #include <util/ieee_float.h>
 #include <util/make_unique.h>
 #include <util/simplify_expr.h>

src/analyses/variable-sensitivity/interval_abstract_value.cpp

@@ -9,9 +9,9 @@
 #include <limits.h>
 #include <ostream>
 
+#include <util/bitvector_types.h>
 #include <util/invariant.h>
 #include <util/make_unique.h>
-#include <util/std_expr.h>
 
 #include "abstract_environment.h"
 

src/ansi-c/gcc_types.h

@@ -9,7 +9,7 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_ANSI_C_GCC_TYPES_H
 #define CPROVER_ANSI_C_GCC_TYPES_H
 
-#include <util/std_types.h>
+#include <util/bitvector_types.h>
 
 // These are gcc-specific; most are not implemented by clang
 // https://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html

src/ansi-c/padding.cpp

@@ -13,10 +13,11 @@ Author: Daniel Kroening, [email protected]
 
 #include <algorithm>
 
+#include <util/arith_tools.h>
+#include <util/bitvector_types.h>
 #include <util/config.h>
 #include <util/pointer_offset_size.h>
 #include <util/simplify_expr.h>
-#include <util/arith_tools.h>
 
 mp_integer alignment(const typet &type, const namespacet &ns)
 {

src/goto-instrument/accelerate/util.h

@@ -12,7 +12,7 @@ Author: Matt Lewis
 #ifndef CPROVER_GOTO_INSTRUMENT_ACCELERATE_UTIL_H
 #define CPROVER_GOTO_INSTRUMENT_ACCELERATE_UTIL_H
 
-#include <util/std_types.h>
+#include <util/bitvector_types.h>
 
 signedbv_typet signed_poly_type();
 unsignedbv_typet unsigned_poly_type();

src/goto-instrument/dump_c.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "dump_c.h"
 
+#include <util/bitvector_types.h>
 #include <util/byte_operators.h>
 #include <util/config.h>
 #include <util/expr_initializer.h>

src/goto-instrument/stack_depth.cpp

@@ -14,6 +14,7 @@ Date: November 2011
 #include "stack_depth.h"
 
 #include <util/arith_tools.h>
+#include <util/bitvector_types.h>
 
 #include <goto-programs/goto_model.h>
 

src/goto-programs/goto_trace.cpp

@@ -16,6 +16,7 @@ Author: Daniel Kroening
 #include <ostream>
 
 #include <util/arith_tools.h>
+#include <util/bitvector_types.h>
 #include <util/byte_operators.h>
 #include <util/format_expr.h>
 #include <util/merge_irep.h>

src/goto-programs/process_goto_program.cpp

@@ -26,6 +26,7 @@ Author: Martin Brain, [email protected]
 #include <goto-programs/string_abstraction.h>
 #include <goto-programs/string_instrumentation.h>
 
+#include <util/bitvector_types.h>
 #include <util/message.h>
 #include <util/options.h>
 

src/goto-programs/string_abstraction.h

@@ -12,9 +12,10 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_GOTO_PROGRAMS_STRING_ABSTRACTION_H
 #define CPROVER_GOTO_PROGRAMS_STRING_ABSTRACTION_H
 
-#include <util/symbol_table.h>
+#include <util/bitvector_types.h>
 #include <util/config.h>
 #include <util/std_expr.h>
+#include <util/symbol_table.h>
 
 #include "goto_model.h"
 

src/goto-symex/partial_order_concurrency.cpp

@@ -14,6 +14,7 @@ Author: Michael Tautschnig, [email protected]
 #include <limits>
 
 #include <util/arith_tools.h>
+#include <util/bitvector_types.h>
 #include <util/simplify_expr.h>
 
 partial_order_concurrencyt::partial_order_concurrencyt(

src/jsil/jsil_typecheck.cpp

@@ -11,9 +11,10 @@ Author: Michael Tautschnig, [email protected]
 
 #include "jsil_typecheck.h"
 
-#include <util/symbol_table.h>
+#include <util/bitvector_types.h>
 #include <util/prefix.h>
 #include <util/std_expr.h>
+#include <util/symbol_table.h>
 
 #include "expr2jsil.h"
 #include "jsil_types.h"

src/jsil/jsil_types.cpp

@@ -11,6 +11,8 @@ Author: Daiva Naudziuniene, [email protected]
 
 #include "jsil_types.h"
 
+#include <util/bitvector_types.h>
+
 #include <algorithm>
 
 typet jsil_any_type()

src/solvers/flattening/boolbv.cpp

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/arith_tools.h>
 #include <util/bitvector_expr.h>
+#include <util/bitvector_types.h>
 #include <util/floatbv_expr.h>
 #include <util/magic.h>
 #include <util/mp_arith.h>

src/solvers/flattening/boolbv_abs.cpp

@@ -8,10 +8,10 @@ Author: Daniel Kroening, [email protected]
 
 #include "boolbv.h"
 
-#include <util/std_types.h>
-
 #include "boolbv_type.h"
 
+#include <util/bitvector_types.h>
+
 #include <solvers/floatbv/float_utils.h>
 
 bvt boolbvt::convert_abs(const abs_exprt &expr)

src/solvers/flattening/boolbv_add_sub.cpp

@@ -8,8 +8,8 @@ Author: Daniel Kroening, [email protected]
 
 #include "boolbv.h"
 
+#include <util/bitvector_types.h>
 #include <util/invariant.h>
-#include <util/std_types.h>
 
 #include <solvers/floatbv/float_utils.h>
 

src/solvers/flattening/boolbv_bv_rel.cpp

@@ -8,7 +8,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "boolbv.h"
 
-#include <util/std_types.h>
+#include <util/bitvector_types.h>
 
 #include "boolbv_type.h"
 

src/solvers/flattening/boolbv_div.cpp

@@ -8,7 +8,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "boolbv.h"
 
-#include <util/std_types.h>
+#include <util/bitvector_types.h>
 
 bvt boolbvt::convert_div(const div_exprt &expr)
 {

src/solvers/flattening/boolbv_extractbit.cpp

@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/arith_tools.h>
 #include <util/bitvector_expr.h>
+#include <util/bitvector_types.h>
 #include <util/exception_utils.h>
 #include <util/std_expr.h>
 #include <util/std_types.h>

src/solvers/flattening/boolbv_floatbv_op.cpp

@@ -11,8 +11,8 @@ Author: Daniel Kroening, [email protected]
 #include <algorithm>
 #include <iostream>
 
+#include <util/bitvector_types.h>
 #include <util/floatbv_expr.h>
-#include <util/std_types.h>
 
 #include <solvers/floatbv/float_utils.h>
 

src/solvers/flattening/boolbv_ieee_float_rel.cpp

@@ -8,10 +8,10 @@ Author: Daniel Kroening, [email protected]
 
 #include "boolbv.h"
 
-#include <util/std_types.h>
-
 #include "boolbv_type.h"
 
+#include <util/bitvector_types.h>
+
 #include <solvers/floatbv/float_utils.h>
 
 literalt boolbvt::convert_ieee_float_rel(const binary_relation_exprt &expr)

src/solvers/flattening/boolbv_mult.cpp

@@ -8,7 +8,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "boolbv.h"
 
-#include <util/std_types.h>
+#include <util/bitvector_types.h>
 
 bvt boolbvt::convert_mult(const mult_exprt &expr)
 {

src/solvers/flattening/boolbv_not.cpp

@@ -6,9 +6,10 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
-
 #include "boolbv.h"
 
+#include <util/bitvector_types.h>
+
 bvt boolbvt::convert_not(const not_exprt &expr)
 {
   const bvt &op_bv=convert_bv(expr.op());

src/solvers/flattening/boolbv_reduction.cpp

@@ -6,9 +6,10 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
-
 #include "boolbv.h"
 
+#include <util/bitvector_types.h>
+
 literalt boolbvt::convert_reduction(const unary_exprt &expr)
 {
   const bvt &op_bv=convert_bv(expr.op());

src/solvers/flattening/boolbv_typecast.cpp

@@ -8,13 +8,13 @@ Author: Daniel Kroening, [email protected]
 
 #include "boolbv.h"
 
-#include <util/std_types.h>
-
-#include <solvers/floatbv/float_utils.h>
-
 #include "boolbv_type.h"
 #include "c_bit_field_replacement_type.h"
 
+#include <util/bitvector_types.h>
+
+#include <solvers/floatbv/float_utils.h>
+
 bvt boolbvt::convert_bv_typecast(const typecast_exprt &expr)
 {
   const exprt &op=expr.op();

src/solvers/flattening/boolbv_unary_minus.cpp

@@ -8,7 +8,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "boolbv.h"
 
-#include <util/std_types.h>
+#include <util/bitvector_types.h>
 
 #include <solvers/floatbv/float_utils.h>
 

src/solvers/flattening/c_bit_field_replacement_type.cpp

@@ -8,6 +8,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "c_bit_field_replacement_type.h"
 
+#include <util/bitvector_types.h>
 #include <util/invariant.h>
 
 typet c_bit_field_replacement_type(

src/solvers/floatbv/float_bv.cpp

@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/arith_tools.h>
 #include <util/bitvector_expr.h>
+#include <util/bitvector_types.h>
 #include <util/floatbv_expr.h>
 #include <util/std_expr.h>
 

src/solvers/lowering/popcount.cpp

@@ -10,9 +10,9 @@ Author: Michael Tautschnig
 
 #include <util/arith_tools.h>
 #include <util/bitvector_expr.h>
+#include <util/bitvector_types.h>
 #include <util/invariant.h>
 #include <util/pointer_offset_size.h>
-#include <util/std_expr.h>
 
 exprt lower_popcount(const popcount_exprt &expr, const namespacet &ns)
 {

src/solvers/refinement/refine_arithmetic.cpp

@@ -9,6 +9,7 @@ Author: Daniel Kroening, [email protected]
 #include "bv_refinement.h"
 
 #include <util/arith_tools.h>
+#include <util/bitvector_types.h>
 #include <util/bv_arithmetic.h>
 #include <util/expr_util.h>
 #include <util/floatbv_expr.h>

src/solvers/smt2/smt2_format.cpp

@@ -9,8 +9,7 @@ Author: Daniel Kroening, [email protected]
 #include "smt2_format.h"
 
 #include <util/arith_tools.h>
-#include <util/std_expr.h>
-#include <util/std_types.h>
+#include <util/bitvector_types.h>
 
 std::ostream &smt2_format_rec(std::ostream &out, const typet &type)
 {

src/solvers/smt2/smt2_parser.cpp

@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/arith_tools.h>
 #include <util/bitvector_expr.h>
+#include <util/bitvector_types.h>
 #include <util/floatbv_expr.h>
 #include <util/ieee_float.h>
 #include <util/invariant.h>

src/statement-list/converters/convert_dint_literal.cpp

@@ -12,10 +12,11 @@ Author: Matthias Weiss, [email protected]
 #include "convert_dint_literal.h"
 #include "statement_list_types.h"
 
+#include <util/arith_tools.h>
+#include <util/bitvector_types.h>
+
 #include <algorithm>
 #include <stdexcept>
-#include <util/arith_tools.h>
-#include <util/std_types.h>
 
 /// Minimum value of double integer literals.
 #define STL_DINT_MAX_VALUE 2147483647LL

src/statement-list/converters/convert_int_literal.cpp

@@ -13,10 +13,11 @@ Author: Matthias Weiss, [email protected]
 #include "convert_dint_literal.h"
 #include "statement_list_types.h"
 
+#include <util/arith_tools.h>
+#include <util/bitvector_types.h>
+
 #include <algorithm>
 #include <stdexcept>
-#include <util/arith_tools.h>
-#include <util/std_types.h>
 
 /// Maximum value of integer literals.
 #define STL_INT_MAX_VALUE 32767LL

src/statement-list/converters/convert_real_literal.cpp

@@ -12,6 +12,7 @@ Author: Matthias Weiss, [email protected]
 #include "convert_real_literal.h"
 #include "statement_list_types.h"
 
+#include <util/bitvector_types.h>
 #include <util/ieee_float.h>
 #include <util/std_expr.h>
 

src/statement-list/converters/statement_list_types.cpp

@@ -10,8 +10,9 @@ Author: Matthias Weiss, [email protected]
 /// Statement List Type Helper
 
 #include "statement_list_types.h"
+
+#include <util/bitvector_types.h>
 #include <util/ieee_float.h>
-#include <util/std_types.h>
 
 signedbv_typet get_int_type()
 {

src/statement-list/parser.y

@@ -17,7 +17,9 @@
 #include "statement_list_parser.h"
 #include "converters/convert_string_value.h"
 #include "converters/statement_list_types.h"
-#include <util/std_expr.h>
+
+#include <util/bitvector_types.h>
+
 #include <iterator>
 
 int yystatement_listlex();