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 
34  // the STL implementation shipped with GCC 5 is broken
35 #if !defined(__GLIBCXX__) || __GLIBCXX__ >= 20181026
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 
155 {
156  PRECONDITION(type.has_subtype());
157  return static_cast<const type_with_subtypet &>(type);
158 }
159 
161 {
162  PRECONDITION(type.has_subtype());
163  return static_cast<type_with_subtypet &>(type);
164 }
165 
168 {
169 public:
170  typedef std::vector<typet> subtypest;
171 
172  type_with_subtypest(const irep_idt &_id, const subtypest &_subtypes)
173  : typet(_id)
174  {
175  subtypes() = _subtypes;
176  }
177 
178  type_with_subtypest(const irep_idt &_id, subtypest &&_subtypes) : typet(_id)
179  {
180  subtypes() = std::move(_subtypes);
181  }
182 
184  {
185  return (subtypest &)get_sub();
186  }
187 
188  const subtypest &subtypes() const
189  {
190  return (const subtypest &)get_sub();
191  }
192 
193  void move_to_subtypes(typet &type); // destroys type
194 
195  void copy_to_subtypes(const typet &type);
196 };
197 
199 {
200  return static_cast<const type_with_subtypest &>(type);
201 }
202 
204 {
205  return static_cast<type_with_subtypest &>(type);
206 }
207 
210 typet remove_const(typet type);
211 
212 #endif // CPROVER_UTIL_TYPE_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:383
subt & get_sub()
Definition: irep.h:466
irept & add(const irep_namet &name)
Definition: irep.cpp:113
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
Type with multiple subtypes.
Definition: type.h:168
type_with_subtypest(const irep_idt &_id, const subtypest &_subtypes)
Definition: type.h:172
void move_to_subtypes(typet &type)
Move the provided type to the subtypes of this type.
Definition: type.cpp:25
subtypest & subtypes()
Definition: type.h:183
std::vector< typet > subtypest
Definition: type.h:170
type_with_subtypest(const irep_idt &_id, subtypest &&_subtypes)
Definition: type.h:178
void copy_to_subtypes(const typet &type)
Copy the provided type to the subtypes of this type.
Definition: type.cpp:17
const subtypest & subtypes() const
Definition: type.h:188
Type with a single subtype.
Definition: type.h:146
type_with_subtypet(irep_idt _id, typet _subtype)
Definition: type.h:148
The type of an expression, extends irept.
Definition: type.h:28
const source_locationt & source_location() const
Definition: type.h:71
typet(irep_idt _id, typet _subtype)
Definition: type.h:36
const typet & subtype() const
Definition: type.h:47
typet(const irep_idt &_id)
Definition: type.h:32
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
bool has_subtypes() const
Definition: type.h:62
const typet & find_type(const irep_namet &name) const
Definition: type.h:86
typet()
Definition: type.h:30
bool has_subtype() const
Definition: type.h:65
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_type(const irep_namet &name)
Definition: type.h:81
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
void remove_subtype()
Definition: type.h:68
typet & subtype()
Definition: type.h:54
source_locationt & add_source_location()
Definition: type.h:76
const irept & get_nil_irep()
Definition: irep.cpp:26
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
const type_with_subtypest & to_type_with_subtypes(const typet &type)
Definition: type.h:198
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition: type.h:154
typet remove_const(typet type)
Remove const qualifier from type (if any).
Definition: type.cpp:32
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)
void validate_type(const typet &type, const namespacet &ns, const validation_modet vm)
Check that the given type is well-formed, assuming that its subtypes have already been checked for we...
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)
validation_modet