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