diff --git a/scripts/expected_doxygen_warnings.txt b/scripts/expected_doxygen_warnings.txt index 4d4dc4d03bd..fa4ca6e397a 100644 --- a/scripts/expected_doxygen_warnings.txt +++ b/scripts/expected_doxygen_warnings.txt @@ -22,7 +22,7 @@ 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 (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 'c_types.h' not generated, too many nodes (110), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. +warning: Included by graph for 'c_types.h' not generated, too many nodes (141), 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. warning: Included by graph for 'expr.h' not generated, too many nodes (87), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. @@ -31,10 +31,10 @@ warning: Included by graph for 'invariant.h' not generated, too many nodes (186) warning: Included by graph for 'irep.h' not generated, too many nodes (62), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'message.h' not generated, too many nodes (117), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'namespace.h' not generated, too many nodes (109), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. -warning: Included by graph for 'pointer_expr.h' not generated, too many nodes (117), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. +warning: Included by graph for 'pointer_expr.h' not generated, too many nodes (116), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'prefix.h' not generated, too many nodes (85), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'simplify_expr.h' not generated, too many nodes (79), 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 (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 'std_types.h' not generated, too many nodes (96), 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. diff --git a/src/ansi-c/c_typecheck_base.h b/src/ansi-c/c_typecheck_base.h index 8213563e595..2791da7a694 100644 --- a/src/ansi-c/c_typecheck_base.h +++ b/src/ansi-c/c_typecheck_base.h @@ -13,10 +13,10 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_ANSI_C_C_TYPECHECK_BASE_H #include +#include #include #include #include -#include #include #include diff --git a/src/ansi-c/padding.cpp b/src/ansi-c/padding.cpp index b6691b2e139..dc6db820078 100644 --- a/src/ansi-c/padding.cpp +++ b/src/ansi-c/padding.cpp @@ -14,7 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include #include #include diff --git a/src/ansi-c/type2name.cpp b/src/ansi-c/type2name.cpp index 314742e5951..48b1631399c 100644 --- a/src/ansi-c/type2name.cpp +++ b/src/ansi-c/type2name.cpp @@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include "type2name.h" #include +#include #include #include #include diff --git a/src/cpp/cpp_exception_id.cpp b/src/cpp/cpp_exception_id.cpp index 2450665753f..b8c9d97e2a4 100644 --- a/src/cpp/cpp_exception_id.cpp +++ b/src/cpp/cpp_exception_id.cpp @@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include "cpp_exception_id.h" +#include #include #include diff --git a/src/cpp/expr2cpp.cpp b/src/cpp/expr2cpp.cpp index 008f24f0678..8b816689883 100644 --- a/src/cpp/expr2cpp.cpp +++ b/src/cpp/expr2cpp.cpp @@ -8,6 +8,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include "expr2cpp.h" +#include #include #include #include diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp index 6fe778a03ae..95191baaa79 100644 --- a/src/goto-instrument/dump_c.cpp +++ b/src/goto-instrument/dump_c.cpp @@ -11,8 +11,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "dump_c.h" -#include #include +#include #include #include #include diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp index 55a08d14696..74e771d0270 100644 --- a/src/goto-programs/goto_trace.cpp +++ b/src/goto-programs/goto_trace.cpp @@ -16,8 +16,8 @@ Author: Daniel Kroening #include #include -#include #include +#include #include #include #include diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp index 606b35803f4..f3280d7adb1 100644 --- a/src/goto-programs/interpreter.cpp +++ b/src/goto-programs/interpreter.cpp @@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp index 41be802d58e..299fb456f22 100644 --- a/src/goto-programs/interpreter_evaluate.cpp +++ b/src/goto-programs/interpreter_evaluate.cpp @@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include diff --git a/src/goto-programs/json_expr.cpp b/src/goto-programs/json_expr.cpp index b857f01489b..7fc7aae16b0 100644 --- a/src/goto-programs/json_expr.cpp +++ b/src/goto-programs/json_expr.cpp @@ -12,6 +12,7 @@ Author: Peter Schrammel #include "json_expr.h" #include +#include #include #include #include diff --git a/src/goto-programs/xml_expr.cpp b/src/goto-programs/xml_expr.cpp index 7b6a810d35b..e797667fd20 100644 --- a/src/goto-programs/xml_expr.cpp +++ b/src/goto-programs/xml_expr.cpp @@ -14,6 +14,7 @@ Author: Daniel Kroening #include "xml_expr.h" #include +#include #include #include #include diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index e188f5cc989..66afccdbbd2 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include diff --git a/src/jsil/jsil_types.h b/src/jsil/jsil_types.h index b3b5a159b40..ab74bf5e4c0 100644 --- a/src/jsil/jsil_types.h +++ b/src/jsil/jsil_types.h @@ -12,8 +12,7 @@ Author: Daiva Naudziuniene, daivan@amazon.com #ifndef CPROVER_JSIL_JSIL_TYPES_H #define CPROVER_JSIL_JSIL_TYPES_H -#include -#include +#include typet jsil_kind(); typet jsil_any_type(); diff --git a/src/linking/linking.cpp b/src/linking/linking.cpp index c7fe2097c93..4fce039fe9d 100644 --- a/src/linking/linking.cpp +++ b/src/linking/linking.cpp @@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include diff --git a/src/solvers/flattening/boolbv_update.cpp b/src/solvers/flattening/boolbv_update.cpp index 3c054cdd37d..058541e3adb 100644 --- a/src/solvers/flattening/boolbv_update.cpp +++ b/src/solvers/flattening/boolbv_update.cpp @@ -9,6 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "boolbv.h" #include +#include bvt boolbvt::convert_update(const update_exprt &expr) { diff --git a/src/solvers/flattening/boolbv_width.cpp b/src/solvers/flattening/boolbv_width.cpp index 5f9777371d9..df15d3a6e8b 100644 --- a/src/solvers/flattening/boolbv_width.cpp +++ b/src/solvers/flattening/boolbv_width.cpp @@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include diff --git a/src/solvers/flattening/boolbv_with.cpp b/src/solvers/flattening/boolbv_with.cpp index d770a75712d..84ee3ef0048 100644 --- a/src/solvers/flattening/boolbv_with.cpp +++ b/src/solvers/flattening/boolbv_with.cpp @@ -8,10 +8,11 @@ Author: Daniel Kroening, kroening@kroening.com #include "boolbv.h" -#include -#include #include +#include #include +#include +#include bvt boolbvt::convert_with(const with_exprt &expr) { diff --git a/src/solvers/flattening/c_bit_field_replacement_type.cpp b/src/solvers/flattening/c_bit_field_replacement_type.cpp index 07f7aa638af..39a7962e0cd 100644 --- a/src/solvers/flattening/c_bit_field_replacement_type.cpp +++ b/src/solvers/flattening/c_bit_field_replacement_type.cpp @@ -8,7 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "c_bit_field_replacement_type.h" -#include +#include #include typet c_bit_field_replacement_type( diff --git a/src/solvers/flattening/c_bit_field_replacement_type.h b/src/solvers/flattening/c_bit_field_replacement_type.h index cc139e96836..e94fc6b6bd0 100644 --- a/src/solvers/flattening/c_bit_field_replacement_type.h +++ b/src/solvers/flattening/c_bit_field_replacement_type.h @@ -10,7 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_SOLVERS_FLATTENING_C_BIT_FIELD_REPLACEMENT_TYPE_H #define CPROVER_SOLVERS_FLATTENING_C_BIT_FIELD_REPLACEMENT_TYPE_H -#include +#include #include typet c_bit_field_replacement_type( diff --git a/src/solvers/smt2/smt2_conv.h b/src/solvers/smt2/smt2_conv.h index 42b2cdfe9d7..4104ed9c7f3 100644 --- a/src/solvers/smt2/smt2_conv.h +++ b/src/solvers/smt2/smt2_conv.h @@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include diff --git a/src/util/arith_tools.cpp b/src/util/arith_tools.cpp index 08075d31649..6d6f672aec9 100644 --- a/src/util/arith_tools.cpp +++ b/src/util/arith_tools.cpp @@ -8,10 +8,10 @@ Author: Daniel Kroening, kroening@kroening.com #include "arith_tools.h" +#include "c_types.h" #include "fixedbv.h" #include "ieee_float.h" #include "invariant.h" -#include "pointer_expr.h" #include "std_expr.h" #include "std_types.h" diff --git a/src/util/c_types.cpp b/src/util/c_types.cpp index bd0a6b268a0..a54ac084d44 100644 --- a/src/util/c_types.cpp +++ b/src/util/c_types.cpp @@ -6,12 +6,12 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ +#include "c_types.h" -#include "std_types.h" #include "config.h" #include "invariant.h" - -#include "c_types.h" +#include "pointer_offset_size.h" +#include "std_types.h" bitvector_typet index_type() { @@ -303,3 +303,34 @@ std::string c_type_as_string(const irep_idt &c_type) else return ""; } + +optionalt> +union_typet::find_widest_union_component(const namespacet &ns) const +{ + const union_typet::componentst &comps = components(); + + optionalt max_width; + typet max_comp_type; + irep_idt max_comp_name; + + for(const auto &comp : comps) + { + auto element_width = pointer_offset_bits(comp.type(), ns); + + if(!element_width.has_value()) + return {}; + + if(max_width.has_value() && *element_width <= *max_width) + continue; + + max_width = *element_width; + max_comp_type = comp.type(); + max_comp_name = comp.get_name(); + } + + if(!max_width.has_value()) + return {}; + else + return std::make_pair( + struct_union_typet::componentt{max_comp_name, max_comp_type}, *max_width); +} diff --git a/src/util/c_types.h b/src/util/c_types.h index d3ad77bd776..df00070581a 100644 --- a/src/util/c_types.h +++ b/src/util/c_types.h @@ -11,7 +11,321 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_UTIL_C_TYPES_H #include "pointer_expr.h" -#include "std_types.h" + +/// Type for C bit fields +/// These are both 'bitvector_typet' (they have a width) +/// and 'type_with_subtypet' (they have a subtype) +class c_bit_field_typet : public bitvector_typet +{ +public: + explicit c_bit_field_typet(typet _subtype, std::size_t width) + : bitvector_typet(ID_c_bit_field, width) + { + subtype().swap(_subtype); + } + + // These have a sub-type +}; + +/// Check whether a reference to a typet is a \ref c_bit_field_typet. +/// \param type: Source type. +/// \return True if \p type is a \ref c_bit_field_typet. +template <> +inline bool can_cast_type(const typet &type) +{ + return type.id() == ID_c_bit_field; +} + +/// \brief Cast a typet to a \ref c_bit_field_typet +/// +/// This is an unchecked conversion. \a type must be known to be \ref +/// c_bit_field_typet. Will fail with a precondition violation if type +/// doesn't match. +/// +/// \param type: Source type. +/// \return Object of type \ref c_bit_field_typet. +inline const c_bit_field_typet &to_c_bit_field_type(const typet &type) +{ + PRECONDITION(can_cast_type(type)); + return static_cast(type); +} + +/// \copydoc to_c_bit_field_type(const typet &type) +inline c_bit_field_typet &to_c_bit_field_type(typet &type) +{ + PRECONDITION(can_cast_type(type)); + return static_cast(type); +} + +/// The C/C++ Booleans +class c_bool_typet : public bitvector_typet +{ +public: + explicit c_bool_typet(std::size_t width) : bitvector_typet(ID_c_bool, width) + { + } + + static void check( + const typet &type, + const validation_modet vm = validation_modet::INVARIANT) + { + DATA_CHECK(vm, !type.get(ID_width).empty(), "C bool type must have width"); + } +}; + +/// Check whether a reference to a typet is a \ref c_bool_typet. +/// \param type: Source type. +/// \return True if \p type is a \ref c_bool_typet. +template <> +inline bool can_cast_type(const typet &type) +{ + return type.id() == ID_c_bool; +} + +/// \brief Cast a typet to a \ref c_bool_typet +/// +/// This is an unchecked conversion. \a type must be known to be \ref +/// c_bool_typet. Will fail with a precondition violation if type +/// doesn't match. +/// +/// \param type: Source type. +/// \return Object of type \ref c_bool_typet. +inline const c_bool_typet &to_c_bool_type(const typet &type) +{ + PRECONDITION(can_cast_type(type)); + c_bool_typet::check(type); + return static_cast(type); +} + +/// \copydoc to_c_bool_type(const typet &) +inline c_bool_typet &to_c_bool_type(typet &type) +{ + PRECONDITION(can_cast_type(type)); + c_bool_typet::check(type); + return static_cast(type); +} + +/// The union type +/// +/// For example, C union. +class union_typet : public struct_union_typet +{ +public: + union_typet() : struct_union_typet(ID_union) + { + } + + explicit union_typet(componentst _components) + : struct_union_typet(ID_union, std::move(_components)) + { + } + + /// Determine the member of maximum bit width in a union type. If no member, + /// or a member of non-fixed width can be found, return nullopt. + /// \param ns: Namespace to resolve tag types. + /// \return Pair of a componentt pointing to the maximum fixed bit-width + /// member of the union type and the bit width of that member. + optionalt> + find_widest_union_component(const namespacet &ns) const; +}; + +/// Check whether a reference to a typet is a \ref union_typet. +/// \param type: Source type. +/// \return True if \p type is a \ref union_typet. +template <> +inline bool can_cast_type(const typet &type) +{ + return type.id() == ID_union; +} + +/// \brief Cast a typet to a \ref union_typet +/// +/// This is an unchecked conversion. \a type must be known to be \ref +/// union_typet. Will fail with a precondition violation if type +/// doesn't match. +/// +/// \param type: Source type. +/// \return Object of type \ref union_typet +inline const union_typet &to_union_type(const typet &type) +{ + PRECONDITION(can_cast_type(type)); + return static_cast(type); +} + +/// \copydoc to_union_type(const typet &) +inline union_typet &to_union_type(typet &type) +{ + PRECONDITION(can_cast_type(type)); + return static_cast(type); +} + +/// A union tag type, i.e., \ref union_typet with an identifier +class union_tag_typet : public tag_typet +{ +public: + explicit union_tag_typet(const irep_idt &identifier) + : tag_typet(ID_union_tag, identifier) + { + } +}; + +/// Check whether a reference to a typet is a \ref union_tag_typet. +/// \param type: Source type. +/// \return True if \p type is a \ref union_tag_typet. +template <> +inline bool can_cast_type(const typet &type) +{ + return type.id() == ID_union_tag; +} + +/// \brief Cast a typet to a \ref union_tag_typet +/// +/// This is an unchecked conversion. \a type must be known to be \ref +/// union_tag_typet. Will fail with a precondition violation if type +/// doesn't match. +/// +/// \param type: Source type. +/// \return Object of type \ref union_tag_typet. +inline const union_tag_typet &to_union_tag_type(const typet &type) +{ + PRECONDITION(can_cast_type(type)); + return static_cast(type); +} + +/// \copydoc to_union_tag_type(const typet &) +inline union_tag_typet &to_union_tag_type(typet &type) +{ + PRECONDITION(can_cast_type(type)); + return static_cast(type); +} + +/// The type of C enums +class c_enum_typet : public type_with_subtypet +{ +public: + explicit c_enum_typet(typet _subtype) + : type_with_subtypet(ID_c_enum, std::move(_subtype)) + { + } + + class c_enum_membert : public irept + { + public: + irep_idt get_value() const + { + return get(ID_value); + } + void set_value(const irep_idt &value) + { + set(ID_value, value); + } + irep_idt get_identifier() const + { + return get(ID_identifier); + } + void set_identifier(const irep_idt &identifier) + { + set(ID_identifier, identifier); + } + irep_idt get_base_name() const + { + return get(ID_base_name); + } + void set_base_name(const irep_idt &base_name) + { + set(ID_base_name, base_name); + } + }; + + typedef std::vector memberst; + + const memberst &members() const + { + return (const memberst &)(find(ID_body).get_sub()); + } + + /// enum types may be incomplete + bool is_incomplete() const + { + return get_bool(ID_incomplete); + } + + /// enum types may be incomplete + void make_incomplete() + { + set(ID_incomplete, true); + } +}; + +/// Check whether a reference to a typet is a \ref c_enum_typet. +/// \param type: Source type. +/// \return True if \p type is a \ref c_enum_typet. +template <> +inline bool can_cast_type(const typet &type) +{ + return type.id() == ID_c_enum; +} + +/// \brief Cast a typet to a \ref c_enum_typet +/// +/// This is an unchecked conversion. \a type must be known to be \ref +/// c_enum_typet. Will fail with a precondition violation if type +/// doesn't match. +/// +/// \param type: Source type. +/// \return Object of type \ref c_enum_typet. +inline const c_enum_typet &to_c_enum_type(const typet &type) +{ + PRECONDITION(can_cast_type(type)); + return static_cast(type); +} + +/// \copydoc to_c_enum_type(const typet &) +inline c_enum_typet &to_c_enum_type(typet &type) +{ + PRECONDITION(can_cast_type(type)); + return static_cast(type); +} + +/// C enum tag type, i.e., \ref c_enum_typet with an identifier +class c_enum_tag_typet : public tag_typet +{ +public: + explicit c_enum_tag_typet(const irep_idt &identifier) + : tag_typet(ID_c_enum_tag, identifier) + { + } +}; + +/// Check whether a reference to a typet is a \ref c_enum_tag_typet. +/// \param type: Source type. +/// \return True if \p type is a \ref c_enum_tag_typet. +template <> +inline bool can_cast_type(const typet &type) +{ + return type.id() == ID_c_enum_tag; +} + +/// \brief Cast a typet to a \ref c_enum_tag_typet +/// +/// This is an unchecked conversion. \a type must be known to be \ref +/// c_enum_tag_typet. Will fail with a precondition violation if type +/// doesn't match. +/// +/// \param type: Source type. +/// \return Object of type \ref c_enum_tag_typet. +inline const c_enum_tag_typet &to_c_enum_tag_type(const typet &type) +{ + PRECONDITION(can_cast_type(type)); + return static_cast(type); +} + +/// \copydoc to_c_enum_tag_type(const typet &) +inline c_enum_tag_typet &to_c_enum_tag_type(typet &type) +{ + PRECONDITION(can_cast_type(type)); + return static_cast(type); +} bitvector_typet index_type(); bitvector_typet enum_constant_type(); diff --git a/src/util/endianness_map.cpp b/src/util/endianness_map.cpp index 25c419a386c..d861d9aa33d 100644 --- a/src/util/endianness_map.cpp +++ b/src/util/endianness_map.cpp @@ -10,10 +10,10 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include "std_types.h" -#include "pointer_offset_size.h" #include "arith_tools.h" +#include "c_types.h" #include "namespace.h" +#include "pointer_offset_size.h" void endianness_mapt::output(std::ostream &out) const { diff --git a/src/util/expr_util.cpp b/src/util/expr_util.cpp index b21716ab2dc..dd24c1802f8 100644 --- a/src/util/expr_util.cpp +++ b/src/util/expr_util.cpp @@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include "arith_tools.h" +#include "c_types.h" #include "expr.h" #include "expr_iterator.h" #include "fixedbv.h" diff --git a/src/util/find_symbols.cpp b/src/util/find_symbols.cpp index 70b3d033931..7b672ba67f0 100644 --- a/src/util/find_symbols.cpp +++ b/src/util/find_symbols.cpp @@ -8,6 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "find_symbols.h" +#include "c_types.h" #include "expr_iterator.h" #include "range.h" #include "std_expr.h" diff --git a/src/util/format_type.cpp b/src/util/format_type.cpp index 69a09485957..f9d9f09d47c 100644 --- a/src/util/format_type.cpp +++ b/src/util/format_type.cpp @@ -7,9 +7,9 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ #include "format_type.h" +#include "c_types.h" #include "format_expr.h" #include "pointer_expr.h" -#include "std_types.h" #include diff --git a/src/util/namespace.cpp b/src/util/namespace.cpp index 827d59fdc09..e0a89679a80 100644 --- a/src/util/namespace.cpp +++ b/src/util/namespace.cpp @@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include "c_types.h" #include "prefix.h" #include "std_expr.h" #include "std_types.h" diff --git a/src/util/simplify_expr_floatbv.cpp b/src/util/simplify_expr_floatbv.cpp index f228ad44803..73c6ab8f601 100644 --- a/src/util/simplify_expr_floatbv.cpp +++ b/src/util/simplify_expr_floatbv.cpp @@ -9,7 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "simplify_expr_class.h" #include "arith_tools.h" -#include "bitvector_types.h" +#include "c_types.h" #include "expr.h" #include "expr_util.h" #include "floatbv_expr.h" diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp index 2c7e555d939..8d1141e8a5d 100644 --- a/src/util/simplify_expr_int.cpp +++ b/src/util/simplify_expr_int.cpp @@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "arith_tools.h" #include "bitvector_expr.h" #include "byte_operators.h" +#include "c_types.h" #include "config.h" #include "expr_util.h" #include "fixedbv.h" diff --git a/src/util/simplify_expr_struct.cpp b/src/util/simplify_expr_struct.cpp index 9a8afc58485..6c7f9430b6f 100644 --- a/src/util/simplify_expr_struct.cpp +++ b/src/util/simplify_expr_struct.cpp @@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "arith_tools.h" #include "byte_operators.h" +#include "c_types.h" #include "invariant.h" #include "namespace.h" #include "pointer_offset_size.h" diff --git a/src/util/simplify_utils.cpp b/src/util/simplify_utils.cpp index 74d618c32de..b6cc3f740b5 100644 --- a/src/util/simplify_utils.cpp +++ b/src/util/simplify_utils.cpp @@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "arith_tools.h" #include "byte_operators.h" +#include "c_types.h" #include "config.h" #include "endianness_map.h" #include "namespace.h" diff --git a/src/util/std_types.cpp b/src/util/std_types.cpp index 9f34fcdf6c3..2d6f55acc2e 100644 --- a/src/util/std_types.cpp +++ b/src/util/std_types.cpp @@ -249,34 +249,3 @@ constant_exprt &vector_typet::size() { return static_cast(add(ID_size)); } - -optionalt> -union_typet::find_widest_union_component(const namespacet &ns) const -{ - const union_typet::componentst &comps = components(); - - optionalt max_width; - typet max_comp_type; - irep_idt max_comp_name; - - for(const auto &comp : comps) - { - auto element_width = pointer_offset_bits(comp.type(), ns); - - if(!element_width.has_value()) - return {}; - - if(max_width.has_value() && *element_width <= *max_width) - continue; - - max_width = *element_width; - max_comp_type = comp.type(); - max_comp_name = comp.get_name(); - } - - if(!max_width.has_value()) - return {}; - else - return std::make_pair( - struct_union_typet::componentt{max_comp_name, max_comp_type}, *max_width); -} diff --git a/src/util/std_types.h b/src/util/std_types.h index dda86d086fe..3c91431fe60 100644 --- a/src/util/std_types.h +++ b/src/util/std_types.h @@ -386,60 +386,6 @@ inline class_typet &to_class_type(typet &type) return static_cast(type); } -/// The union type -/// -/// For example, C union. -class union_typet:public struct_union_typet -{ -public: - union_typet():struct_union_typet(ID_union) - { - } - - explicit union_typet(componentst _components) - : struct_union_typet(ID_union, std::move(_components)) - { - } - - /// Determine the member of maximum bit width in a union type. If no member, - /// or a member of non-fixed width can be found, return nullopt. - /// \param ns: Namespace to resolve tag types. - /// \return Pair of a componentt pointing to the maximum fixed bit-width - /// member of the union type and the bit width of that member. - optionalt> - find_widest_union_component(const namespacet &ns) const; -}; - -/// Check whether a reference to a typet is a \ref union_typet. -/// \param type: Source type. -/// \return True if \p type is a \ref union_typet. -template <> -inline bool can_cast_type(const typet &type) -{ - return type.id() == ID_union; -} - -/// \brief Cast a typet to a \ref union_typet -/// -/// This is an unchecked conversion. \a type must be known to be \ref -/// union_typet. Will fail with a precondition violation if type -/// doesn't match. -/// -/// \param type: Source type. -/// \return Object of type \ref union_typet -inline const union_typet &to_union_type(const typet &type) -{ - PRECONDITION(can_cast_type(type)); - return static_cast(type); -} - -/// \copydoc to_union_type(const typet &) -inline union_typet &to_union_type(typet &type) -{ - PRECONDITION(can_cast_type(type)); - return static_cast(type); -} - /// A tag-based type, i.e., \ref typet with an identifier class tag_typet:public typet { @@ -533,46 +479,6 @@ inline struct_tag_typet &to_struct_tag_type(typet &type) return static_cast(type); } -/// A union tag type, i.e., \ref union_typet with an identifier -class union_tag_typet:public tag_typet -{ -public: - explicit union_tag_typet(const irep_idt &identifier): - tag_typet(ID_union_tag, identifier) - { - } -}; - -/// Check whether a reference to a typet is a \ref union_tag_typet. -/// \param type: Source type. -/// \return True if \p type is a \ref union_tag_typet. -template <> -inline bool can_cast_type(const typet &type) -{ - return type.id() == ID_union_tag; -} - -/// \brief Cast a typet to a \ref union_tag_typet -/// -/// This is an unchecked conversion. \a type must be known to be \ref -/// union_tag_typet. Will fail with a precondition violation if type -/// doesn't match. -/// -/// \param type: Source type. -/// \return Object of type \ref union_tag_typet. -inline const union_tag_typet &to_union_tag_type(const typet &type) -{ - PRECONDITION(can_cast_type(type)); - return static_cast(type); -} - -/// \copydoc to_union_tag_type(const typet &) -inline union_tag_typet &to_union_tag_type(typet &type) -{ - PRECONDITION(can_cast_type(type)); - return static_cast(type); -} - /// An enumeration type, i.e., a type with elements (not to be confused with C /// enums) class enumeration_typet:public typet @@ -623,122 +529,6 @@ inline enumeration_typet &to_enumeration_type(typet &type) return static_cast(type); } -/// The type of C enums -class c_enum_typet:public type_with_subtypet -{ -public: - explicit c_enum_typet(typet _subtype) - : type_with_subtypet(ID_c_enum, std::move(_subtype)) - { - } - - class c_enum_membert:public irept - { - public: - irep_idt get_value() const { return get(ID_value); } - void set_value(const irep_idt &value) { set(ID_value, value); } - irep_idt get_identifier() const { return get(ID_identifier); } - void set_identifier(const irep_idt &identifier) - { - set(ID_identifier, identifier); - } - irep_idt get_base_name() const { return get(ID_base_name); } - void set_base_name(const irep_idt &base_name) - { - set(ID_base_name, base_name); - } - }; - - typedef std::vector memberst; - - const memberst &members() const - { - return (const memberst &)(find(ID_body).get_sub()); - } - - /// enum types may be incomplete - bool is_incomplete() const - { - return get_bool(ID_incomplete); - } - - /// enum types may be incomplete - void make_incomplete() - { - set(ID_incomplete, true); - } -}; - -/// Check whether a reference to a typet is a \ref c_enum_typet. -/// \param type: Source type. -/// \return True if \p type is a \ref c_enum_typet. -template <> -inline bool can_cast_type(const typet &type) -{ - return type.id() == ID_c_enum; -} - -/// \brief Cast a typet to a \ref c_enum_typet -/// -/// This is an unchecked conversion. \a type must be known to be \ref -/// c_enum_typet. Will fail with a precondition violation if type -/// doesn't match. -/// -/// \param type: Source type. -/// \return Object of type \ref c_enum_typet. -inline const c_enum_typet &to_c_enum_type(const typet &type) -{ - PRECONDITION(can_cast_type(type)); - return static_cast(type); -} - -/// \copydoc to_c_enum_type(const typet &) -inline c_enum_typet &to_c_enum_type(typet &type) -{ - PRECONDITION(can_cast_type(type)); - return static_cast(type); -} - -/// C enum tag type, i.e., \ref c_enum_typet with an identifier -class c_enum_tag_typet:public tag_typet -{ -public: - explicit c_enum_tag_typet(const irep_idt &identifier): - tag_typet(ID_c_enum_tag, identifier) - { - } -}; - -/// Check whether a reference to a typet is a \ref c_enum_tag_typet. -/// \param type: Source type. -/// \return True if \p type is a \ref c_enum_tag_typet. -template <> -inline bool can_cast_type(const typet &type) -{ - return type.id() == ID_c_enum_tag; -} - -/// \brief Cast a typet to a \ref c_enum_tag_typet -/// -/// This is an unchecked conversion. \a type must be known to be \ref -/// c_enum_tag_typet. Will fail with a precondition violation if type -/// doesn't match. -/// -/// \param type: Source type. -/// \return Object of type \ref c_enum_tag_typet. -inline const c_enum_tag_typet &to_c_enum_tag_type(const typet &type) -{ - PRECONDITION(can_cast_type(type)); - return static_cast(type); -} - -/// \copydoc to_c_enum_tag_type(const typet &) -inline c_enum_tag_typet &to_c_enum_tag_type(typet &type) -{ - PRECONDITION(can_cast_type(type)); - return static_cast(type); -} - /// Base type of functions class code_typet:public typet { @@ -1078,100 +868,6 @@ inline bool can_cast_type(const typet &type) type.id() == ID_c_bool; } -/// Type for C bit fields -/// These are both 'bitvector_typet' (they have a width) -/// and 'type_with_subtypet' (they have a subtype) -class c_bit_field_typet:public bitvector_typet -{ -public: - explicit c_bit_field_typet(typet _subtype, std::size_t width) - : bitvector_typet(ID_c_bit_field, width) - { - subtype().swap(_subtype); - } - - // These have a sub-type -}; - -/// Check whether a reference to a typet is a \ref c_bit_field_typet. -/// \param type: Source type. -/// \return True if \p type is a \ref c_bit_field_typet. -template <> -inline bool can_cast_type(const typet &type) -{ - return type.id() == ID_c_bit_field; -} - -/// \brief Cast a typet to a \ref c_bit_field_typet -/// -/// This is an unchecked conversion. \a type must be known to be \ref -/// c_bit_field_typet. Will fail with a precondition violation if type -/// doesn't match. -/// -/// \param type: Source type. -/// \return Object of type \ref c_bit_field_typet. -inline const c_bit_field_typet &to_c_bit_field_type(const typet &type) -{ - PRECONDITION(can_cast_type(type)); - return static_cast(type); -} - -/// \copydoc to_c_bit_field_type(const typet &type) -inline c_bit_field_typet &to_c_bit_field_type(typet &type) -{ - PRECONDITION(can_cast_type(type)); - return static_cast(type); -} - -/// The C/C++ Booleans -class c_bool_typet:public bitvector_typet -{ -public: - explicit c_bool_typet(std::size_t width): - bitvector_typet(ID_c_bool, width) - { - } - - static void check( - const typet &type, - const validation_modet vm = validation_modet::INVARIANT) - { - DATA_CHECK(vm, !type.get(ID_width).empty(), "C bool type must have width"); - } -}; - -/// Check whether a reference to a typet is a \ref c_bool_typet. -/// \param type: Source type. -/// \return True if \p type is a \ref c_bool_typet. -template <> -inline bool can_cast_type(const typet &type) -{ - return type.id() == ID_c_bool; -} - -/// \brief Cast a typet to a \ref c_bool_typet -/// -/// This is an unchecked conversion. \a type must be known to be \ref -/// c_bool_typet. Will fail with a precondition violation if type -/// doesn't match. -/// -/// \param type: Source type. -/// \return Object of type \ref c_bool_typet. -inline const c_bool_typet &to_c_bool_type(const typet &type) -{ - PRECONDITION(can_cast_type(type)); - c_bool_typet::check(type); - return static_cast(type); -} - -/// \copydoc to_c_bool_type(const typet &) -inline c_bool_typet &to_c_bool_type(typet &type) -{ - PRECONDITION(can_cast_type(type)); - c_bool_typet::check(type); - return static_cast(type); -} - /// String type /// /// Represents string constants, such as `@class_identifier`. diff --git a/src/util/validate_types.cpp b/src/util/validate_types.cpp index a68b05b3975..af2b810db04 100644 --- a/src/util/validate_types.cpp +++ b/src/util/validate_types.cpp @@ -12,9 +12,9 @@ Author: Daniel Poetzl #include #endif +#include "c_types.h" #include "namespace.h" #include "pointer_expr.h" -#include "type.h" #include "validate.h" #include "validate_helpers.h" diff --git a/unit/analyses/constant_propagator.cpp b/unit/analyses/constant_propagator.cpp index fffd27f79d1..e2a69bb0f14 100644 --- a/unit/analyses/constant_propagator.cpp +++ b/unit/analyses/constant_propagator.cpp @@ -14,7 +14,7 @@ Author: Diffblue Ltd #include #include -#include +#include #include #include diff --git a/unit/util/expr.cpp b/unit/util/expr.cpp index d3c08c17477..61f089ecb93 100644 --- a/unit/util/expr.cpp +++ b/unit/util/expr.cpp @@ -9,7 +9,7 @@ Author: Diffblue Ltd #include #include -#include +#include #include #include