cprover
type.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_UTIL_TYPE_H
11 #define CPROVER_UTIL_TYPE_H
12 
13 #include "source_location.h"
14 
15 #define SUBTYPE_IN_GETSUB
16 #define SUBTYPES_IN_GETSUB
17 
18 class namespacet;
19 
22 class typet:public irept
23 {
24 public:
25  typet() { }
26 
27  explicit typet(const irep_idt &_id):irept(_id) { }
28  typet(const irep_idt &_id, const typet &_subtype):irept(_id)
29  {
30  subtype()=_subtype;
31  }
32 
33  const typet &subtype() const
34  #ifdef SUBTYPE_IN_GETSUB
35  {
36  if(get_sub().empty())
37  return static_cast<const typet &>(get_nil_irep());
38  return static_cast<const typet &>(get_sub().front());
39  }
40  #else
41  { return (typet &)find(ID_subtype); }
42  #endif
43 
45  #ifdef SUBTYPE_IN_GETSUB
46  {
47  subt &sub=get_sub();
48  if(sub.empty())
49  sub.resize(1);
50  return static_cast<typet &>(sub.front());
51  }
52  #else
53  { return (typet &)add(ID_subtype); }
54  #endif
55 
56  typedef std::vector<typet> subtypest;
57 
59  #ifdef SUBTYPES_IN_GETSUB
60  { return (subtypest &)get_sub(); }
61  #else
62  { return (subtypest &)add(ID_subtypes).get_sub(); }
63  #endif
64 
65  const subtypest &subtypes() const
66  #ifdef SUBTYPES_IN_GETSUB
67  { return (const subtypest &)get_sub(); }
68  #else
69  { return (const subtypest &)find(ID_subtypes).get_sub(); }
70  #endif
71 
72  bool has_subtypes() const
73  #ifdef SUBTYPES_IN_GETSUB
74  { return !get_sub().empty(); }
75  #else
76  { return !find(ID_subtypes).is_nil(); }
77  #endif
78 
79  bool has_subtype() const
80  #ifdef SUBTYPE_IN_GETSUB
81  { return !get_sub().empty(); }
82  #else
83  { return !find(ID_subtype).is_nil(); }
84  #endif
85 
87  #ifdef SUBTYPE_IN_GETSUB
88  { get_sub().clear(); }
89  #else
90  { remove(ID_subtype); }
91  #endif
92 
93  void move_to_subtypes(typet &type); // destroys expr
94 
95  void copy_to_subtypes(const typet &type);
96 
98  {
99  return (const source_locationt &)find(ID_C_source_location);
100  }
101 
103  {
104  return static_cast<source_locationt &>(add(ID_C_source_location));
105  }
106 
107  typet &add_type(const irep_namet &name)
108  {
109  return static_cast<typet &>(add(name));
110  }
111 
112  const typet &find_type(const irep_namet &name) const
113  {
114  return static_cast<const typet &>(find(name));
115  }
116 };
117 
119 {
120 public:
122 
123  explicit type_with_subtypet(const irep_idt &_id):typet(_id) { }
124  type_with_subtypet(const irep_idt &_id, const typet &_subtype):
125  typet(_id)
126  {
127  subtype()=_subtype;
128  }
129 
130  #if 0
131  const typet &subtype() const
132  { return (typet &)find(ID_subtype); }
133 
134  typet &subtype()
135  { return (typet &)add(ID_subtype); }
136  #endif
137 };
138 
140 {
141 public:
143 
144  explicit type_with_subtypest(const irep_idt &_id):typet(_id) { }
145 
146  #if 0
147  typedef std::vector<typet> subtypest;
148 
150  { return (subtypest &)add(ID_subtypes).get_sub(); }
151 
152  const subtypest &subtypes() const
153  { return (const subtypest &)find(ID_subtypes).get_sub(); }
154 
155  void move_to_subtypes(typet &type); // destroys expr
156 
157  void copy_to_subtypes(const typet &type);
158  #endif
159 };
160 
161 #define forall_subtypes(it, type) \
162  if((type).has_subtypes()) /* NOLINT(readability/braces) */ \
163  for(typet::subtypest::const_iterator it=(type).subtypes().begin(), \
164  it##_end=(type).subtypes().end(); \
165  it!=it##_end; ++it)
166 
167 #define Forall_subtypes(it, type) \
168  if((type).has_subtypes()) /* NOLINT(readability/braces) */ \
169  for(typet::subtypest::iterator it=(type).subtypes().begin(); \
170  it!=(type).subtypes().end(); ++it)
171 
172 /*
173 
174 pre-defined types:
175  universe // super type
176  type // another type
177  predicate // predicate expression (subtype and predicate)
178  uninterpreted // uninterpreted type with identifier
179  empty // void
180  bool // true or false
181  abstract // abstract super type
182  struct // with components: each component has name and type
183  // the ordering matters
184  rational
185  real
186  integer
187  complex
188  string
189  enum // with elements
190  // the ordering does not matter
191  tuple // with components: each component has type
192  // the ordering matters
193  mapping // domain -> range
194  bv // no interpretation
195  unsignedbv
196  signedbv // two's complement
197  floatbv // IEEE floating point format
198  code
199  pointer // for ANSI-C (subtype)
200  symbol // look in symbol table (identifier)
201  number // generic number super type
202 
203 */
204 
205 bool is_number(const typet &type);
206 // rational, real, integer, complex, unsignedbv, signedbv, floatbv
207 
208 // Is the passed in type const qualified?
210  const typet &type,
211  const namespacet &ns);
212 
213 #endif // CPROVER_UTIL_TYPE_H
const irept & get_nil_irep()
Definition: irep.cpp:56
The type of an expression.
Definition: type.h:22
bool has_subtypes() const
Definition: type.h:72
typet(const irep_idt &_id)
Definition: type.h:27
bool is_nil() const
Definition: irep.h:102
type_with_subtypet(const irep_idt &_id)
Definition: type.h:123
bool has_subtype() const
Definition: type.h:79
std::vector< irept > subt
Definition: irep.h:90
subtypest & subtypes()
Definition: type.h:58
type_with_subtypet(const irep_idt &_id, const typet &_subtype)
Definition: type.h:124
typet()
Definition: type.h:25
void move_to_subtypes(typet &type)
Definition: type.cpp:18
type_with_subtypest(const irep_idt &_id)
Definition: type.h:144
subt & get_sub()
Definition: irep.h:245
typet(const irep_idt &_id, const typet &_subtype)
Definition: type.h:28
void remove_subtype()
Definition: type.h:86
bool is_number(const typet &type)
Definition: type.cpp:25
TO_BE_DOCUMENTED.
Definition: namespace.h:74
void copy_to_subtypes(const typet &type)
Definition: type.cpp:13
Base class for tree-like data structures with sharing.
Definition: irep.h:86
std::vector< typet > subtypest
Definition: type.h:56
type_with_subtypet()
Definition: type.h:121
const source_locationt & source_location() const
Definition: type.h:97
const typet & find_type(const irep_namet &name) const
Definition: type.h:112
typet & subtype()
Definition: type.h:44
const subtypest & subtypes() const
Definition: type.h:65
source_locationt & add_source_location()
Definition: type.h:102
irept & add(const irep_namet &name)
Definition: irep.cpp:306
typet & add_type(const irep_namet &name)
Definition: type.h:107
const typet & subtype() const
Definition: type.h:33
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
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