cprover
type.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "type.h"
10 #include "std_types.h"
11 #include "namespace.h"
12 
13 void typet::copy_to_subtypes(const typet &type)
14 {
15  subtypes().push_back(type);
16 }
17 
19 {
20  subtypest &sub=subtypes();
21  sub.push_back(static_cast<const typet &>(get_nil_irep()));
22  sub.back().swap(type);
23 }
24 
25 bool is_number(const typet &type)
26 {
27  const irep_idt &id=type.id();
28  return id==ID_rational ||
29  id==ID_real ||
30  id==ID_integer ||
31  id==ID_natural ||
32  id==ID_complex ||
33  id==ID_unsignedbv ||
34  id==ID_signedbv ||
35  id==ID_floatbv ||
36  id==ID_fixedbv;
37 }
38 
48  const typet &type, const namespacet &ns)
49 {
50  // Helper function to avoid the code duplication in the branches
51  // below.
52  const auto has_constant_components =
53  [&ns](const typet &subtype) -> bool
54  {
55  if(subtype.id() == ID_struct || subtype.id() == ID_union)
56  {
57  const auto &struct_union_type = to_struct_union_type(subtype);
58  for(const auto &component : struct_union_type.components())
59  {
60  if(is_constant_or_has_constant_components(component.type(), ns))
61  return true;
62  }
63  }
64  return false;
65  };
66 
67  // There are 4 possibilities the code below is handling.
68  // The possibilities are enumerated as comments, to show
69  // what each code is supposed to be handling. For more
70  // comprehensive test case for this, take a look at
71  // regression/cbmc/no_nondet_static/main.c
72 
73  // const int a;
74  if(type.get_bool(ID_C_constant))
75  return true;
76 
77  // This is a termination condition to break the recursion
78  // for recursive types such as the following:
79  // struct list { const int datum; struct list * next; };
80  // NOTE: the difference between this condition and the previous
81  // one is that this one always returns.
82  if(type.id()==ID_pointer)
83  return type.get_bool(ID_C_constant);
84 
85  // When we have a case like the following, we don't immediately
86  // see the struct t. Instead, we only get to see symbol t1, which
87  // we have to use the namespace to resolve to its definition:
88  // struct t { const int a; };
89  // struct t t1;
90  if(type.id() == ID_symbol)
91  {
92  const auto &resolved_type = ns.follow(type);
93  return has_constant_components(resolved_type);
94  }
95 
96  // In a case like this, where we see an array (b[3] here), we know that
97  // the array contains subtypes. We get the first one, and
98  // then resolve it to its definition through the usage of the namespace.
99  // struct contains_constant_pointer { int x; int * const p; };
100  // struct contains_constant_pointer b[3] = { {23, &y}, {23, &y}, {23, &y} };
101  if(type.has_subtype())
102  {
103  const auto &subtype = type.subtype();
104  return is_constant_or_has_constant_components(subtype, ns);
105  }
106 
107  return false;
108 }
const irept & get_nil_irep()
Definition: irep.cpp:56
The type of an expression.
Definition: type.h:22
bool has_subtype() const
Definition: type.h:79
subtypest & subtypes()
Definition: type.h:58
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
void move_to_subtypes(typet &type)
Definition: type.cpp:18
const irep_idt & id() const
Definition: irep.h:259
TO_BE_DOCUMENTED.
Definition: namespace.h:74
void copy_to_subtypes(const typet &type)
Definition: type.cpp:13
bool is_constant_or_has_constant_components(const typet &type, const namespacet &ns)
Identify if a given type is constant itself or contains constant components.
Definition: type.cpp:47
const typet & follow(const typet &) const
Definition: namespace.cpp:55
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
std::vector< typet > subtypest
Definition: type.h:56
API to type classes.
bool is_number(const typet &type)
Definition: type.cpp:25
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
Definition: std_types.h:280
const typet & subtype() const
Definition: type.h:33