Merge pull request #2991 from diffblue/type-cleanup

cleanup accesses to subtype() and subtypes()

Author: Daniel Kroening

src/util/mathematical_types.h

@@ -55,7 +55,7 @@ class real_typet : public typet
 
 /// A type for mathematical functions (do not confuse with functions/methods
 /// in code)
-class mathematical_function_typet : public typet
+class mathematical_function_typet : public type_with_subtypest
 {
 public:
   // the domain of the function is composed of zero, one, or
@@ -88,7 +88,7 @@ class mathematical_function_typet : public typet
   using domaint = std::vector<variablet>;
 
   mathematical_function_typet(const domaint &_domain, const typet &_codomain)
-    : typet(ID_mathematical_function)
+    : type_with_subtypest(ID_mathematical_function)
   {
     subtypes().resize(2);
     domain() = _domain;
@@ -97,12 +97,12 @@ class mathematical_function_typet : public typet
 
   domaint &domain()
   {
-    return (domaint &)subtypes()[0].subtypes();
+    return (domaint &)to_type_with_subtypes(subtypes()[0]).subtypes();
   }
 
   const domaint &domain() const
   {
-    return (const domaint &)subtypes()[0].subtypes();
+    return (const domaint &)to_type_with_subtypes(subtypes()[0]).subtypes();
   }
 
   variablet &add_variable()

src/util/type.h

@@ -110,6 +110,18 @@ class type_with_subtypet:public typet
   #endif
 };
 
+inline const type_with_subtypet &to_type_with_subtype(const typet &type)
+{
+  PRECONDITION(type.has_subtype());
+  return static_cast<const type_with_subtypet &>(type);
+}
+
+inline type_with_subtypet &to_type_with_subtype(typet &type)
+{
+  PRECONDITION(type.has_subtype());
+  return static_cast<type_with_subtypet &>(type);
+}
+
 /// Type with multiple subtypes.
 class type_with_subtypest:public typet
 {
@@ -133,15 +145,25 @@ class type_with_subtypest:public typet
   #endif
 };
 
+inline const type_with_subtypest &to_type_with_subtypes(const typet &type)
+{
+  return static_cast<const type_with_subtypest &>(type);
+}
+
+inline type_with_subtypest &to_type_with_subtypes(typet &type)
+{
+  return static_cast<type_with_subtypest &>(type);
+}
+
 #define forall_subtypes(it, type) \
   if((type).has_subtypes()) /* NOLINT(readability/braces) */ \
-    for(typet::subtypest::const_iterator it=(type).subtypes().begin(), \
-        it##_end=(type).subtypes().end(); \
+    for(type_with_subtypest::subtypest::const_iterator it=to_type_with_subtypes(type).subtypes().begin(), \
+        it##_end=to_type_with_subtypes(type).subtypes().end(); \
         it!=it##_end; ++it)
 
 #define Forall_subtypes(it, type) \
   if((type).has_subtypes()) /* NOLINT(readability/braces) */ \
-    for(typet::subtypest::iterator it=(type).subtypes().begin(); \
-        it!=(type).subtypes().end(); ++it)
+    for(type_with_subtypest::subtypest::iterator it=to_type_with_subtypes(type).subtypes().begin(); \
+        it!=to_type_with_subtypes(type).subtypes().end(); ++it)
 
 #endif // CPROVER_UTIL_TYPE_H