Move functions from type to std_types

Author: svorenova

jbmc/src/java_bytecode/ci_lazy_methods_needed.h

@@ -12,10 +12,11 @@ Author: Chris Smowton, [email protected]
 #ifndef CPROVER_JAVA_BYTECODE_CI_LAZY_METHODS_H
 #define CPROVER_JAVA_BYTECODE_CI_LAZY_METHODS_H
 
-#include <vector>
 #include <set>
 #include <unordered_set>
+#include <util/namespace.h>
 #include <util/symbol_table.h>
+#include <vector>
 
 class select_pointer_typet;
 class pointer_typet;

src/util/std_types.cpp

@@ -12,9 +12,10 @@ Author: Daniel Kroening, [email protected]
 
 #include "std_types.h"
 
-#include "string2int.h"
 #include "arith_tools.h"
+#include "namespace.h"
 #include "std_expr.h"
+#include "string2int.h"
 
 std::size_t fixedbv_typet::get_integer_bits() const
 {
@@ -195,3 +196,84 @@ constant_exprt unsignedbv_typet::largest_expr() const
 {
   return from_integer(largest(), *this);
 }
+
+/// Returns true if the type is a rational, real, integer, natural, complex,
+/// unsignedbv, signedbv, floatbv or fixedbv.
+bool is_number(const typet &type)
+{
+  const irep_idt &id = type.id();
+  return id == ID_rational || id == ID_real || id == ID_integer ||
+         id == ID_natural || id == ID_complex || id == ID_unsignedbv ||
+         id == ID_signedbv || id == ID_floatbv || id == ID_fixedbv;
+}
+
+/// Identify whether a given type is constant itself or contains constant
+/// components.
+/// Examples include:
+///  - const int a;
+///  - struct contains_constant_pointer {  int x; int * const p; };
+///  - const int b[3];
+/// \param type The type we want to query constness of.
+/// \param ns The namespace, needed for resolution of symbols.
+/// \return Whether passed in type is const or not.
+bool is_constant_or_has_constant_components(
+  const typet &type,
+  const namespacet &ns)
+{
+  // Helper function to avoid the code duplication in the branches
+  // below.
+  const auto has_constant_components = [&ns](const typet &subtype) -> bool {
+    if(subtype.id() == ID_struct || subtype.id() == ID_union)
+    {
+      const auto &struct_union_type = to_struct_union_type(subtype);
+      for(const auto &component : struct_union_type.components())
+      {
+        if(is_constant_or_has_constant_components(component.type(), ns))
+          return true;
+      }
+    }
+    return false;
+  };
+
+  // There are 4 possibilities the code below is handling.
+  // The possibilities are enumerated as comments, to show
+  // what each code is supposed to be handling. For more
+  // comprehensive test case for this, take a look at
+  // regression/cbmc/no_nondet_static/main.c
+
+  // const int a;
+  if(type.get_bool(ID_C_constant))
+    return true;
+
+  // This is a termination condition to break the recursion
+  // for recursive types such as the following:
+  // struct list { const int datum; struct list * next; };
+  // NOTE: the difference between this condition and the previous
+  // one is that this one always returns.
+  if(type.id() == ID_pointer)
+    return type.get_bool(ID_C_constant);
+
+  // When we have a case like the following, we don't immediately
+  // see the struct t. Instead, we only get to see symbol t1, which
+  // we have to use the namespace to resolve to its definition:
+  // struct t { const int a; };
+  // struct t t1;
+  if(type.id() == ID_symbol_type)
+  {
+    const auto &resolved_type = ns.follow(type);
+    return has_constant_components(resolved_type);
+  }
+
+  // In a case like this, where we see an array (b[3] here), we know that
+  // the array contains subtypes. We get the first one, and
+  // then resolve it to its  definition through the usage of the namespace.
+  // struct contains_constant_pointer { int x; int * const p; };
+  // struct contains_constant_pointer b[3] = { {23, &y}, {23, &y}, {23, &y} };
+  if(type.has_subtype())
+  {
+    const auto &subtype = type.subtype();
+    return is_constant_or_has_constant_components(subtype, ns);
+  }
+
+  return false;
+}

src/util/std_types.h

@@ -21,6 +21,7 @@ Author: Daniel Kroening, [email protected]
 #include <unordered_map>
 
 class constant_exprt;
+class namespacet;
 
 /// The Boolean type
 class bool_typet:public typet
@@ -1708,4 +1709,10 @@ inline mathematical_function_typet &
   return static_cast<mathematical_function_typet &>(type);
 }
 
+bool is_number(const typet &type);
+
+bool is_constant_or_has_constant_components(
+  const typet &type,
+  const namespacet &ns);
+
 #endif // CPROVER_UTIL_STD_TYPES_H

src/util/type.cpp

@@ -11,8 +11,6 @@ Author: Daniel Kroening, [email protected]
 /// Implementations of some functions of typet
 
 #include "type.h"
-#include "std_types.h"
-#include "namespace.h"
 
 /// Copy the provided type to the subtypes of this type.
 /// \param type The type to add to subtypes
@@ -30,91 +28,3 @@ void typet::move_to_subtypes(typet &type)
   sub.push_back(static_cast<const typet &>(get_nil_irep()));
   sub.back().swap(type);
 }
-
-/// Returns true if the type is a rational, real, integer, natural, complex,
-/// unsignedbv, signedbv, floatbv or fixedbv.
-bool is_number(const typet &type)
-{
-  const irep_idt &id=type.id();
-  return id==ID_rational ||
-         id==ID_real ||
-         id==ID_integer ||
-         id==ID_natural ||
-         id==ID_complex ||
-         id==ID_unsignedbv ||
-         id==ID_signedbv ||
-         id==ID_floatbv ||
-         id==ID_fixedbv;
-}
-
-/// Identify whether a given type is constant itself or contains constant
-/// components.
-/// Examples include:
-///  - const int a;
-///  - struct contains_constant_pointer {  int x; int * const p; };
-///  - const int b[3];
-/// \param type The type we want to query constness of.
-/// \param ns The namespace, needed for resolution of symbols.
-/// \return Whether passed in type is const or not.
-bool is_constant_or_has_constant_components(
-  const typet &type, const namespacet &ns)
-{
-  // Helper function to avoid the code duplication in the branches
-  // below.
-  const auto has_constant_components =
-    [&ns](const typet &subtype) -> bool
-    {
-      if(subtype.id() == ID_struct || subtype.id() == ID_union)
-      {
-        const auto &struct_union_type = to_struct_union_type(subtype);
-        for(const auto &component : struct_union_type.components())
-        {
-          if(is_constant_or_has_constant_components(component.type(), ns))
-            return true;
-        }
-      }
-      return false;
-    };
-
-  // There are 4 possibilities the code below is handling.
-  // The possibilities are enumerated as comments, to show
-  // what each code is supposed to be handling. For more
-  // comprehensive test case for this, take a look at
-  // regression/cbmc/no_nondet_static/main.c
-
-  // const int a;
-  if(type.get_bool(ID_C_constant))
-    return true;
-
-  // This is a termination condition to break the recursion
-  // for recursive types such as the following:
-  // struct list { const int datum; struct list * next; };
-  // NOTE: the difference between this condition and the previous
-  // one is that this one always returns.
-  if(type.id()==ID_pointer)
-    return type.get_bool(ID_C_constant);
-
-  // When we have a case like the following, we don't immediately
-  // see the struct t. Instead, we only get to see symbol t1, which
-  // we have to use the namespace to resolve to its definition:
-  // struct t { const int a; };
-  // struct t t1;
-  if(type.id() == ID_symbol_type)
-  {
-    const auto &resolved_type = ns.follow(type);
-    return has_constant_components(resolved_type);
-  }
-
-  // In a case like this, where we see an array (b[3] here), we know that
-  // the array contains subtypes. We get the first one, and
-  // then resolve it to its  definition through the usage of the namespace.
-  // struct contains_constant_pointer { int x; int * const p; };
-  // struct contains_constant_pointer b[3] = { {23, &y}, {23, &y}, {23, &y} };
-  if(type.has_subtype())
-  {
-    const auto &subtype = type.subtype();
-    return is_constant_or_has_constant_components(subtype, ns);
-  }
-
-  return false;
-}

src/util/type.h

@@ -18,8 +18,6 @@ Author: Daniel Kroening, [email protected]
 #define SUBTYPE_IN_GETSUB
 #define SUBTYPES_IN_GETSUB
 
-class namespacet;
-
 /// The type of an expression, extends irept. Types may have subtypes. This is
 /// modeled with two subs named “subtype” (a single type) and “subtypes”
 /// (a vector of types). The class typet only adds specialized methods
@@ -177,10 +175,4 @@ class type_with_subtypest:public typet
     for(typet::subtypest::iterator it=(type).subtypes().begin(); \
         it!=(type).subtypes().end(); ++it)
 
-bool is_number(const typet &type);
-
-bool is_constant_or_has_constant_components(
-    const typet &type,
-    const namespacet &ns);
-
 #endif // CPROVER_UTIL_TYPE_H