move the types used in C programs to c_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

src/ansi-c/c_typecheck_base.h

@@ -13,10 +13,10 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_ANSI_C_C_TYPECHECK_BASE_H
 
 #include <util/bitvector_expr.h>
+#include <util/c_types.h>
 #include <util/namespace.h>
 #include <util/std_code.h>
 #include <util/std_expr.h>
-#include <util/std_types.h>
 #include <util/symbol_table.h>
 #include <util/typecheck.h>
 

src/ansi-c/padding.cpp

@@ -14,7 +14,7 @@ Author: Daniel Kroening, [email protected]
 #include <algorithm>
 
 #include <util/arith_tools.h>
-#include <util/bitvector_types.h>
+#include <util/c_types.h>
 #include <util/config.h>
 #include <util/pointer_offset_size.h>
 #include <util/simplify_expr.h>

src/goto-instrument/dump_c.cpp

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

src/goto-programs/interpreter_evaluate.cpp

@@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/bitvector_expr.h>
 #include <util/byte_operators.h>
+#include <util/c_types.h>
 #include <util/fixedbv.h>
 #include <util/ieee_float.h>
 #include <util/pointer_expr.h>

src/goto-programs/json_expr.cpp

@@ -12,6 +12,7 @@ Author: Peter Schrammel
 #include "json_expr.h"
 
 #include <util/arith_tools.h>
+#include <util/c_types.h>
 #include <util/config.h>
 #include <util/expr.h>
 #include <util/expr_util.h>

src/goto-programs/xml_expr.cpp

@@ -14,6 +14,7 @@ Author: Daniel Kroening
 #include "xml_expr.h"
 
 #include <util/arith_tools.h>
+#include <util/c_types.h>
 #include <util/config.h>
 #include <util/expr.h>
 #include <util/fixedbv.h>

src/solvers/flattening/boolbv_width.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 #include <algorithm>
 
 #include <util/arith_tools.h>
+#include <util/c_types.h>
 #include <util/exception_utils.h>
 #include <util/invariant.h>
 #include <util/namespace.h>

src/solvers/flattening/c_bit_field_replacement_type.cpp

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

src/solvers/flattening/c_bit_field_replacement_type.h

@@ -10,7 +10,7 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_SOLVERS_FLATTENING_C_BIT_FIELD_REPLACEMENT_TYPE_H
 #define CPROVER_SOLVERS_FLATTENING_C_BIT_FIELD_REPLACEMENT_TYPE_H
 
-#include <util/std_types.h>
+#include <util/c_types.h>
 #include <util/namespace.h>
 
 typet c_bit_field_replacement_type(

src/util/arith_tools.cpp

@@ -8,10 +8,10 @@ Author: Daniel Kroening, [email protected]
 
 #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"
 

src/util/c_types.h

@@ -11,7 +11,99 @@ Author: Daniel Kroening, [email protected]
 #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<c_bit_field_typet>(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<c_bit_field_typet>(type));
+  return static_cast<const c_bit_field_typet &>(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<c_bit_field_typet>(type));
+  return static_cast<c_bit_field_typet &>(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<c_bool_typet>(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<c_bool_typet>(type));
+  c_bool_typet::check(type);
+  return static_cast<const c_bool_typet &>(type);
+}
+
+/// \copydoc to_c_bool_type(const typet &)
+inline c_bool_typet &to_c_bool_type(typet &type)
+{
+  PRECONDITION(can_cast_type<c_bool_typet>(type));
+  c_bool_typet::check(type);
+  return static_cast<c_bool_typet &>(type);
+}
 
 bitvector_typet index_type();
 bitvector_typet enum_constant_type();

src/util/format_type.cpp

@@ -7,9 +7,9 @@ Author: Daniel Kroening, [email protected]
 \*******************************************************************/
 
 #include "format_type.h"
+#include "c_types.h"
 #include "format_expr.h"
 #include "pointer_expr.h"
-#include "std_types.h"
 
 #include <ostream>
 

src/util/std_types.h

@@ -1078,100 +1078,6 @@ inline bool can_cast_type<bitvector_typet>(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<c_bit_field_typet>(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<c_bit_field_typet>(type));
-  return static_cast<const c_bit_field_typet &>(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<c_bit_field_typet>(type));
-  return static_cast<c_bit_field_typet &>(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<c_bool_typet>(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<c_bool_typet>(type));
-  c_bool_typet::check(type);
-  return static_cast<const c_bool_typet &>(type);
-}
-
-/// \copydoc to_c_bool_type(const typet &)
-inline c_bool_typet &to_c_bool_type(typet &type)
-{
-  PRECONDITION(can_cast_type<c_bool_typet>(type));
-  c_bool_typet::check(type);
-  return static_cast<c_bool_typet &>(type);
-}
-
 /// String type
 ///
 /// Represents string constants, such as `@class_identifier`.

src/util/validate_types.cpp

@@ -12,9 +12,9 @@ Author: Daniel Poetzl
 #include <iostream>
 #endif
 
+#include "c_types.h"
 #include "namespace.h"
 #include "pointer_expr.h"
-#include "type.h"
 #include "validate.h"
 #include "validate_helpers.h"