cprover
type.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Defines typet, type_with_subtypet and type_with_subtypest
4 
5 Author: Daniel Kroening, kroening@kroening.com
6  Maria Svorenova, maria.svorenova@diffblue.com
7 
8 \*******************************************************************/
9 
12 
13 #ifndef CPROVER_UTIL_TYPE_H
14 #define CPROVER_UTIL_TYPE_H
15 
16 class namespacet;
17 
18 #include "source_location.h"
19 #include "validate_types.h"
20 #include "validation_mode.h"
21 
27 class typet:public irept
28 {
29 public:
30  typet() { }
31 
32  explicit typet(const irep_idt &_id):irept(_id) { }
33  typet(const irep_idt &_id, const typet &_subtype):irept(_id)
34  {
35  subtype()=_subtype;
36  }
37 
38  const typet &subtype() const
39  {
40  if(get_sub().empty())
41  return static_cast<const typet &>(get_nil_irep());
42  return static_cast<const typet &>(get_sub().front());
43  }
44 
46  {
47  subt &sub=get_sub();
48  if(sub.empty())
49  sub.resize(1);
50  return static_cast<typet &>(sub.front());
51  }
52 
53  bool has_subtypes() const
54  { return !get_sub().empty(); }
55 
56  bool has_subtype() const
57  { return !get_sub().empty(); }
58 
60  { get_sub().clear(); }
61 
63  {
64  return (const source_locationt &)find(ID_C_source_location);
65  }
66 
68  {
69  return static_cast<source_locationt &>(add(ID_C_source_location));
70  }
71 
72  typet &add_type(const irep_namet &name)
73  {
74  return static_cast<typet &>(add(name));
75  }
76 
77  const typet &find_type(const irep_namet &name) const
78  {
79  return static_cast<const typet &>(find(name));
80  }
81 
90  static void check(const typet &, const validation_modet)
91  {
92  }
93 
102  static void validate(
103  const typet &type,
104  const namespacet &,
106  {
107  check_type(type, vm);
108  }
109 
118  static void validate_full(
119  const typet &type,
120  const namespacet &ns,
122  {
123  // check subtypes
124  for(const irept &sub : type.get_sub())
125  {
126  const typet &subtype = static_cast<const typet &>(sub);
127  validate_full_type(subtype, ns, vm);
128  }
129 
130  validate_type(type, ns, vm);
131  }
132 };
133 
136 {
137 public:
138  DEPRECATED("use type_with_subtypet(id, subtype) instead")
139  explicit type_with_subtypet(const irep_idt &_id):typet(_id) { }
140 
141  type_with_subtypet(const irep_idt &_id, const typet &_subtype):
142  typet(_id)
143  {
144  subtype()=_subtype;
145  }
146 
147  #if 0
148  const typet &subtype() const
149  { return (typet &)find(ID_subtype); }
150 
151  typet &subtype()
152  { return (typet &)add(ID_subtype); }
153  #endif
154 };
155 
157 {
158  PRECONDITION(type.has_subtype());
159  return static_cast<const type_with_subtypet &>(type);
160 }
161 
163 {
164  PRECONDITION(type.has_subtype());
165  return static_cast<type_with_subtypet &>(type);
166 }
167 
170 {
171 public:
172  typedef std::vector<typet> subtypest;
173 
174  DEPRECATED("use type_with_subtypest(id, subtypes) instead")
176 
177  DEPRECATED("use type_with_subtypest(id, subtypes) instead")
178  explicit type_with_subtypest(const irep_idt &_id):typet(_id) { }
179 
180  type_with_subtypest(const irep_idt &_id, const subtypest &_subtypes)
181  : typet(_id)
182  {
183  subtypes() = _subtypes;
184  }
185 
186  type_with_subtypest(const irep_idt &_id, subtypest &&_subtypes) : typet(_id)
187  {
188  subtypes() = std::move(_subtypes);
189  }
190 
192  {
193  return (subtypest &)get_sub();
194  }
195 
196  const subtypest &subtypes() const
197  {
198  return (const subtypest &)get_sub();
199  }
200 
201  void move_to_subtypes(typet &type); // destroys type
202 
203  void copy_to_subtypes(const typet &type);
204 };
205 
207 {
208  return static_cast<const type_with_subtypest &>(type);
209 }
210 
212 {
213  return static_cast<type_with_subtypest &>(type);
214 }
215 
216 #define forall_subtypes(it, type) \
217  if((type).has_subtypes()) /* NOLINT(readability/braces) */ \
218  for(type_with_subtypest::subtypest::const_iterator it=to_type_with_subtypes(type).subtypes().begin(), \
219  it##_end=to_type_with_subtypes(type).subtypes().end(); \
220  it!=it##_end; ++it)
221 
222 #define Forall_subtypes(it, type) \
223  if((type).has_subtypes()) /* NOLINT(readability/braces) */ \
224  for(type_with_subtypest::subtypest::iterator it=to_type_with_subtypes(type).subtypes().begin(); \
225  it!=to_type_with_subtypes(type).subtypes().end(); ++it)
226 
227 #endif // CPROVER_UTIL_TYPE_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
type_with_subtypest::copy_to_subtypes
void copy_to_subtypes(const typet &type)
Copy the provided type to the subtypes of this type.
Definition: type.cpp:17
typet::subtype
const typet & subtype() const
Definition: type.h:38
type_with_subtypest
Type with multiple subtypes.
Definition: type.h:169
type_with_subtypest::subtypest
std::vector< typet > subtypest
Definition: type.h:172
validate_full_type
void validate_full_type(const typet &type, const namespacet &ns, const validation_modet vm)
Check that the given type is well-formed (full check, including checks of subtypes)
Definition: validate_types.cpp:83
typet
The type of an expression, extends irept.
Definition: type.h:27
typet::has_subtype
bool has_subtype() const
Definition: type.h:56
irept::add
irept & add(const irep_namet &name)
Definition: irep.cpp:305
typet::has_subtypes
bool has_subtypes() const
Definition: type.h:53
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:284
to_type_with_subtype
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition: type.h:156
to_type_with_subtypes
const type_with_subtypest & to_type_with_subtypes(const typet &type)
Definition: type.h:206
type_with_subtypet
Type with a single subtype.
Definition: type.h:135
type_with_subtypest::subtypes
subtypest & subtypes()
Definition: type.h:191
typet::typet
typet()
Definition: type.h:30
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
validate_type
void validate_type(const typet &)
Called after casting.
Definition: expr_cast.h:57
type_with_subtypet::type_with_subtypet
type_with_subtypet(const irep_idt &_id, const typet &_subtype)
Definition: type.h:141
typet::typet
typet(const irep_idt &_id, const typet &_subtype)
Definition: type.h:33
type_with_subtypest::type_with_subtypest
type_with_subtypest(const irep_idt &_id, const subtypest &_subtypes)
Definition: type.h:180
check_type
void check_type(const typet &type, const validation_modet vm)
Check that the given type is well-formed (shallow checks only, i.e., subtypes are not checked)
Definition: validate_types.cpp:54
typet::source_location
const source_locationt & source_location() const
Definition: type.h:62
typet::check
static void check(const typet &, const validation_modet)
Check that the type is well-formed (shallow checks only, i.e., subtypes are not checked)
Definition: type.h:90
type_with_subtypest::move_to_subtypes
void move_to_subtypes(typet &type)
Move the provided type to the subtypes of this type.
Definition: type.cpp:25
source_location.h
typet::remove_subtype
void remove_subtype()
Definition: type.h:59
validation_modet
validation_modet
Definition: validation_mode.h:12
validation_mode.h
typet::add_source_location
source_locationt & add_source_location()
Definition: type.h:67
typet::validate
static void validate(const typet &type, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
Check that the type is well-formed, assuming that its subtypes have already been checked for well-for...
Definition: type.h:102
source_locationt
Definition: source_location.h:20
typet::validate_full
static void validate_full(const typet &type, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Check that the type is well-formed (full check, including checks of subtypes)
Definition: type.h:118
type_with_subtypest::subtypes
const subtypest & subtypes() const
Definition: type.h:196
DEPRECATED
#define DEPRECATED(msg)
Definition: deprecate.h:23
irept::get_sub
subt & get_sub()
Definition: irep.h:317
irept
Base class for tree-like data structures with sharing.
Definition: irep.h:156
get_nil_irep
const irept & get_nil_irep()
Definition: irep.cpp:55
typet::add_type
typet & add_type(const irep_namet &name)
Definition: type.h:72
typet::find_type
const typet & find_type(const irep_namet &name) const
Definition: type.h:77
validate_types.h
typet::subtype
typet & subtype()
Definition: type.h:45
irept::subt
std::vector< irept > subt
Definition: irep.h:160
validation_modet::INVARIANT
@ INVARIANT
typet::typet
typet(const irep_idt &_id)
Definition: type.h:32
type_with_subtypest::type_with_subtypest
type_with_subtypest(const irep_idt &_id, subtypest &&_subtypes)
Definition: type.h:186