move pointer_typet to pointer_expr.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.

src/analyses/variable-sensitivity/abstract_pointer_object.cpp

@@ -9,6 +9,8 @@
 #include <analyses/variable-sensitivity/abstract_environment.h>
 #include <analyses/variable-sensitivity/abstract_pointer_object.h>
 
+#include <util/pointer_expr.h>
+
 abstract_pointer_objectt::abstract_pointer_objectt(const typet &t)
   : abstract_objectt(t)
 {

src/cpp/cpp_is_pod.cpp

@@ -11,6 +11,8 @@ Author: Daniel Kroening, [email protected]
 
 #include "cpp_typecheck.h"
 
+#include <util/pointer_expr.h>
+
 bool cpp_typecheckt::cpp_is_pod(const typet &type) const
 {
   if(type.id()==ID_struct)

src/cpp/cpp_type2name.cpp

@@ -14,7 +14,7 @@ Author: Daniel Kroening, [email protected]
 #include <string>
 
 #include <util/cprover_prefix.h>
-#include <util/std_types.h>
+#include <util/pointer_expr.h>
 #include <util/type.h>
 
 static std::string do_prefix(const std::string &s)

src/cpp/expr2cpp.cpp

@@ -8,12 +8,12 @@ Author: Daniel Kroening, [email protected]
 
 #include "expr2cpp.h"
 
-#include <util/std_types.h>
-#include <util/std_expr.h>
-#include <util/symbol.h>
-#include <util/lispirep.h>
 #include <util/lispexpr.h>
+#include <util/lispirep.h>
 #include <util/namespace.h>
+#include <util/pointer_expr.h>
+#include <util/std_expr.h>
+#include <util/symbol.h>
 
 #include <ansi-c/c_misc.h>
 #include <ansi-c/c_qualifiers.h>

src/goto-programs/xml_expr.cpp

@@ -20,7 +20,7 @@ Author: Daniel Kroening
 #include <util/ieee_float.h>
 #include <util/invariant.h>
 #include <util/namespace.h>
-#include <util/std_expr.h>
+#include <util/pointer_expr.h>
 #include <util/xml.h>
 
 xmlt xml(const typet &type, const namespacet &ns)

src/solvers/flattening/boolbv_width.cpp

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/exception_utils.h>
 #include <util/invariant.h>
 #include <util/namespace.h>
+#include <util/pointer_expr.h>
 #include <util/std_types.h>
 
 boolbv_widtht::boolbv_widtht(const namespacet &_ns):ns(_ns)

src/util/base_type.cpp

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 #include <set>
 
 #include "namespace.h"
+#include "pointer_expr.h"
 #include "std_types.h"
 #include "symbol.h"
 #include "union_find.h"

src/util/c_types.h

@@ -10,6 +10,7 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_UTIL_C_TYPES_H
 #define CPROVER_UTIL_C_TYPES_H
 
+#include "pointer_expr.h"
 #include "std_types.h"
 
 bitvector_typet index_type();

src/util/format_type.cpp

@@ -8,6 +8,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "format_type.h"
 #include "format_expr.h"
+#include "pointer_expr.h"
 #include "std_types.h"
 
 #include <ostream>

src/util/pointer_expr.h

@@ -16,6 +16,131 @@ Author: Daniel Kroening, [email protected]
 
 class namespacet;
 
+/// The pointer type
+/// These are both 'bitvector_typet' (they have a width)
+/// and 'type_with_subtypet' (they have a subtype)
+class pointer_typet : public bitvector_typet
+{
+public:
+  pointer_typet(typet _subtype, std::size_t width)
+    : bitvector_typet(ID_pointer, width)
+  {
+    subtype().swap(_subtype);
+  }
+
+  signedbv_typet difference_type() const
+  {
+    return signedbv_typet(get_width());
+  }
+
+  static void check(
+    const typet &type,
+    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    DATA_CHECK(vm, !type.get(ID_width).empty(), "pointer must have width");
+  }
+};
+
+/// Check whether a reference to a typet is a \ref pointer_typet.
+/// \param type: Source type.
+/// \return True if \p type is a \ref pointer_typet.
+template <>
+inline bool can_cast_type<pointer_typet>(const typet &type)
+{
+  return type.id() == ID_pointer;
+}
+
+/// \brief Cast a typet to a \ref pointer_typet
+///
+/// This is an unchecked conversion. \a type must be known to be \ref
+/// pointer_typet. Will fail with a precondition violation if type
+/// doesn't match.
+///
+/// \param type: Source type.
+/// \return Object of type \ref pointer_typet.
+inline const pointer_typet &to_pointer_type(const typet &type)
+{
+  PRECONDITION(can_cast_type<pointer_typet>(type));
+  pointer_typet::check(type);
+  return static_cast<const pointer_typet &>(type);
+}
+
+/// \copydoc to_pointer_type(const typet &)
+inline pointer_typet &to_pointer_type(typet &type)
+{
+  PRECONDITION(can_cast_type<pointer_typet>(type));
+  pointer_typet::check(type);
+  return static_cast<pointer_typet &>(type);
+}
+
+/// This method tests,
+/// if the given typet is a pointer of type void.
+inline bool is_void_pointer(const typet &type)
+{
+  return type.id() == ID_pointer && type.subtype().id() == ID_empty;
+}
+
+/// The reference type
+///
+/// Intends to model C++ reference. Comparing to \ref pointer_typet should
+/// never be null.
+class reference_typet : public pointer_typet
+{
+public:
+  reference_typet(typet _subtype, std::size_t _width)
+    : pointer_typet(std::move(_subtype), _width)
+  {
+    set(ID_C_reference, true);
+  }
+
+  static void check(
+    const typet &type,
+    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    PRECONDITION(type.id() == ID_pointer);
+    const reference_typet &reference_type =
+      static_cast<const reference_typet &>(type);
+    DATA_CHECK(
+      vm, !reference_type.get(ID_width).empty(), "reference must have width");
+    DATA_CHECK(
+      vm, reference_type.get_width() > 0, "reference must have non-zero width");
+  }
+};
+
+/// Check whether a reference to a typet is a \ref reference_typet.
+/// \param type: Source type.
+/// \return True if \p type is a \ref reference_typet.
+template <>
+inline bool can_cast_type<reference_typet>(const typet &type)
+{
+  return can_cast_type<pointer_typet>(type) && type.get_bool(ID_C_reference);
+}
+
+/// \brief Cast a typet to a \ref reference_typet
+///
+/// This is an unchecked conversion. \a type must be known to be \ref
+/// reference_typet. Will fail with a precondition violation if type
+/// doesn't match.
+///
+/// \param type: Source type.
+/// \return Object of type \ref reference_typet.
+inline const reference_typet &to_reference_type(const typet &type)
+{
+  PRECONDITION(can_cast_type<reference_typet>(type));
+  return static_cast<const reference_typet &>(type);
+}
+
+/// \copydoc to_reference_type(const typet &)
+inline reference_typet &to_reference_type(typet &type)
+{
+  PRECONDITION(can_cast_type<reference_typet>(type));
+  return static_cast<reference_typet &>(type);
+}
+
+bool is_reference(const typet &type);
+
+bool is_rvalue_reference(const typet &type);
+
 /// \brief Split an expression into a base object and a (byte) offset
 class object_descriptor_exprt : public binary_exprt
 {

src/util/refined_string_type.h

@@ -20,7 +20,7 @@ Author: Romain Brenguier, [email protected]
 #define CPROVER_UTIL_REFINED_STRING_TYPE_H
 
 #include "cprover_prefix.h"
-#include "std_types.h"
+#include "pointer_expr.h"
 
 // Internal type used for string refinement
 class refined_string_typet: public struct_typet

src/util/std_types.h

@@ -1488,131 +1488,6 @@ inline c_bit_field_typet &to_c_bit_field_type(typet &type)
   return static_cast<c_bit_field_typet &>(type);
 }
 
-/// The pointer type
-/// These are both 'bitvector_typet' (they have a width)
-/// and 'type_with_subtypet' (they have a subtype)
-class pointer_typet:public bitvector_typet
-{
-public:
-  pointer_typet(typet _subtype, std::size_t width)
-    : bitvector_typet(ID_pointer, width)
-  {
-    subtype().swap(_subtype);
-  }
-
-  signedbv_typet difference_type() const
-  {
-    return signedbv_typet(get_width());
-  }
-
-  static void check(
-    const typet &type,
-    const validation_modet vm = validation_modet::INVARIANT)
-  {
-    DATA_CHECK(vm, !type.get(ID_width).empty(), "pointer must have width");
-  }
-};
-
-/// Check whether a reference to a typet is a \ref pointer_typet.
-/// \param type: Source type.
-/// \return True if \p type is a \ref pointer_typet.
-template <>
-inline bool can_cast_type<pointer_typet>(const typet &type)
-{
-  return type.id() == ID_pointer;
-}
-
-/// \brief Cast a typet to a \ref pointer_typet
-///
-/// This is an unchecked conversion. \a type must be known to be \ref
-/// pointer_typet. Will fail with a precondition violation if type
-/// doesn't match.
-///
-/// \param type: Source type.
-/// \return Object of type \ref pointer_typet.
-inline const pointer_typet &to_pointer_type(const typet &type)
-{
-  PRECONDITION(can_cast_type<pointer_typet>(type));
-  pointer_typet::check(type);
-  return static_cast<const pointer_typet &>(type);
-}
-
-/// \copydoc to_pointer_type(const typet &)
-inline pointer_typet &to_pointer_type(typet &type)
-{
-  PRECONDITION(can_cast_type<pointer_typet>(type));
-  pointer_typet::check(type);
-  return static_cast<pointer_typet &>(type);
-}
-
-/// This method tests,
-/// if the given typet is a pointer of type void.
-inline bool is_void_pointer(const typet &type)
-{
-  return type.id() == ID_pointer && type.subtype().id() == ID_empty;
-}
-
-/// The reference type
-///
-/// Intends to model C++ reference. Comparing to \ref pointer_typet should
-/// never be null.
-class reference_typet:public pointer_typet
-{
-public:
-  reference_typet(typet _subtype, std::size_t _width)
-    : pointer_typet(std::move(_subtype), _width)
-  {
-    set(ID_C_reference, true);
-  }
-
-  static void check(
-    const typet &type,
-    const validation_modet vm = validation_modet::INVARIANT)
-  {
-    PRECONDITION(type.id() == ID_pointer);
-    const reference_typet &reference_type =
-      static_cast<const reference_typet &>(type);
-    DATA_CHECK(
-      vm, !reference_type.get(ID_width).empty(), "reference must have width");
-    DATA_CHECK(
-      vm, reference_type.get_width() > 0, "reference must have non-zero width");
-  }
-};
-
-/// Check whether a reference to a typet is a \ref reference_typet.
-/// \param type: Source type.
-/// \return True if \p type is a \ref reference_typet.
-template <>
-inline bool can_cast_type<reference_typet>(const typet &type)
-{
-  return can_cast_type<pointer_typet>(type) && type.get_bool(ID_C_reference);
-}
-
-/// \brief Cast a typet to a \ref reference_typet
-///
-/// This is an unchecked conversion. \a type must be known to be \ref
-/// reference_typet. Will fail with a precondition violation if type
-/// doesn't match.
-///
-/// \param type: Source type.
-/// \return Object of type \ref reference_typet.
-inline const reference_typet &to_reference_type(const typet &type)
-{
-  PRECONDITION(can_cast_type<reference_typet>(type));
-  return static_cast<const reference_typet &>(type);
-}
-
-/// \copydoc to_reference_type(const typet &)
-inline reference_typet &to_reference_type(typet &type)
-{
-  PRECONDITION(can_cast_type<reference_typet>(type));
-  return static_cast<reference_typet &>(type);
-}
-
-bool is_reference(const typet &type);
-
-bool is_rvalue_reference(const typet &type);
-
 /// The C/C++ Booleans
 class c_bool_typet:public bitvector_typet
 {

src/util/validate_types.cpp

@@ -13,7 +13,7 @@ Author: Daniel Poetzl
 #endif
 
 #include "namespace.h"
-#include "std_types.h"
+#include "pointer_expr.h"
 #include "type.h"
 #include "validate.h"
 #include "validate_helpers.h"