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 "deprecate.h"
19 #include "source_location.h"
20 #include "validate_types.h"
21 #include "validation_mode.h"
22 
28 class typet:public irept
29 {
30 public:
31  typet() { }
32 
33  explicit typet(const irep_idt &_id):irept(_id) { }
34 
35 #if defined(__clang__) || !defined(__GNUC__) || __GNUC__ >= 6
36  typet(irep_idt _id, typet _subtype)
37  : irept(std::move(_id), {}, {std::move(_subtype)})
38  {
39  }
40 #else
41  typet(irep_idt _id, typet _subtype) : irept(std::move(_id))
42  {
43  subtype() = std::move(_subtype);
44  }
45 #endif
46 
47  const typet &subtype() const
48  {
49  if(get_sub().empty())
50  return static_cast<const typet &>(get_nil_irep());
51  return static_cast<const typet &>(get_sub().front());
52  }
53 
55  {
56  subt &sub=get_sub();
57  if(sub.empty())
58  sub.resize(1);
59  return static_cast<typet &>(sub.front());
60  }
61 
62  bool has_subtypes() const
63  { return !get_sub().empty(); }
64 
65  bool has_subtype() const
66  { return !get_sub().empty(); }
67 
69  { get_sub().clear(); }
70 
72  {
73  return (const source_locationt &)find(ID_C_source_location);
74  }
75 
77  {
78  return static_cast<source_locationt &>(add(ID_C_source_location));
79  }
80 
81  typet &add_type(const irep_namet &name)
82  {
83  return static_cast<typet &>(add(name));
84  }
85 
86  const typet &find_type(const irep_namet &name) const
87  {
88  return static_cast<const typet &>(find(name));
89  }
90 
99  static void
101  {
102  }
103 
112  static void validate(
113  const typet &type,
114  const namespacet &,
116  {
117  check_type(type, vm);
118  }
119 
128  static void validate_full(
129  const typet &type,
130  const namespacet &ns,
132  {
133  // check subtypes
134  for(const irept &sub : type.get_sub())
135  {
136  const typet &subtype = static_cast<const typet &>(sub);
137  validate_full_type(subtype, ns, vm);
138  }
139 
140  validate_type(type, ns, vm);
141  }
142 };
143 
146 {
147 public:
149  : typet(std::move(_id), std::move(_subtype))
150  {
151  }
152 
153  #if 0
154  const typet &subtype() const
155  { return (typet &)find(ID_subtype); }
156 
157  typet &subtype()
158  { return (typet &)add(ID_subtype); }
159  #endif
160 };
161 
163 {
164  PRECONDITION(type.has_subtype());
165  return static_cast<const type_with_subtypet &>(type);
166 }
167 
169 {
170  PRECONDITION(type.has_subtype());
171  return static_cast<type_with_subtypet &>(type);
172 }
173 
176 {
177 public:
178  typedef std::vector<typet> subtypest;
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 
229 typet remove_const(typet type);
230 
231 #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:37
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:47
type_with_subtypest
Type with multiple subtypes.
Definition: type.h:176
type_with_subtypest::subtypest
std::vector< typet > subtypest
Definition: type.h:178
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:103
typet
The type of an expression, extends irept.
Definition: type.h:29
typet::has_subtype
bool has_subtype() const
Definition: type.h:65
irept::add
irept & add(const irep_namet &name)
Definition: irep.cpp:113
typet::has_subtypes
bool has_subtypes() const
Definition: type.h:62
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
to_type_with_subtype
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition: type.h:162
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:146
type_with_subtypest::subtypes
subtypest & subtypes()
Definition: type.h:191
typet::typet
typet()
Definition: type.h:31
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
deprecate.h
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:74
type_with_subtypet::type_with_subtypet
type_with_subtypet(irep_idt _id, typet _subtype)
Definition: type.h:148
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
typet::source_location
const source_locationt & source_location() const
Definition: type.h:71
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
validate_type
void validate_type(const reference_typet &type)
Definition: std_types.h:1571
typet::remove_subtype
void remove_subtype()
Definition: type.h:68
validation_modet
validation_modet
Definition: validation_mode.h:13
validation_mode.h
typet::check
static void check(const typet &, const validation_modet=validation_modet::INVARIANT)
Check that the type is well-formed (shallow checks only, i.e., subtypes are not checked)
Definition: type.h:100
typet::add_source_location
source_locationt & add_source_location()
Definition: type.h:76
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:112
sharing_treet< irept, std::map< irep_namet, irept > >::subt
typename dt::subt subt
Definition: irep.h:182
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:128
type_with_subtypest::subtypes
const subtypest & subtypes() const
Definition: type.h:196
typet::typet
typet(irep_idt _id, typet _subtype)
Definition: type.h:36
irept::get_sub
subt & get_sub()
Definition: irep.h:477
remove_const
typet remove_const(typet type)
Remove const qualifier from type (if any).
Definition: type.cpp:32
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:394
get_nil_irep
const irept & get_nil_irep()
Definition: irep.cpp:26
typet::add_type
typet & add_type(const irep_namet &name)
Definition: type.h:81
typet::find_type
const typet & find_type(const irep_namet &name) const
Definition: type.h:86
validate_types.h
typet::subtype
typet & subtype()
Definition: type.h:54
validation_modet::INVARIANT
@ INVARIANT
typet::typet
typet(const irep_idt &_id)
Definition: type.h:33
type_with_subtypest::type_with_subtypest
type_with_subtypest(const irep_idt &_id, subtypest &&_subtypes)
Definition: type.h:186