cprover
Loading...
Searching...
No Matches
type.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Defines typet, type_with_subtypet and type_with_subtypest
4
5Author: 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
16class namespacet;
17
18#include "source_location.h"
19#include "validate.h"
20#include "validate_types.h"
21#include "validation_mode.h"
22
28class typet:public irept
29{
30public:
31 typet() { }
32
33 explicit typet(const irep_idt &_id):irept(_id) { }
34
35 // the STL implementation shipped with GCC 5 is broken
36#if !defined(__GLIBCXX__) || __GLIBCXX__ >= 20181026
37 typet(irep_idt _id, typet _subtype)
38 : irept(std::move(_id), {}, {std::move(_subtype)})
39 {
40 }
41#else
42 typet(irep_idt _id, typet _subtype) : irept(std::move(_id))
43 {
44 subtype() = std::move(_subtype);
45 }
46#endif
47
48 const typet &subtype() const
49 {
50 if(get_sub().empty())
51 return static_cast<const typet &>(get_nil_irep());
52 return static_cast<const typet &>(get_sub().front());
53 }
54
56 {
57 subt &sub=get_sub();
58 if(sub.empty())
59 sub.resize(1);
60 return static_cast<typet &>(sub.front());
61 }
62
63 bool has_subtypes() const
64 { return !get_sub().empty(); }
65
66 bool has_subtype() const
67 {
68 return get_sub().size() == 1;
69 }
70
72 { get_sub().clear(); }
73
75 {
76 return (const source_locationt &)find(ID_C_source_location);
77 }
78
80 {
81 return static_cast<source_locationt &>(add(ID_C_source_location));
82 }
83
84 typet &add_type(const irep_idt &name)
85 {
86 return static_cast<typet &>(add(name));
87 }
88
89 const typet &find_type(const irep_idt &name) const
90 {
91 return static_cast<const typet &>(find(name));
92 }
93
102 static void
104 {
105 }
106
115 static void validate(
116 const typet &type,
117 const namespacet &,
119 {
120 check_type(type, vm);
121 }
122
131 static void validate_full(
132 const typet &type,
133 const namespacet &ns,
135 {
136 // check subtypes
137 for(const irept &sub : type.get_sub())
138 {
139 const typet &subtype = static_cast<const typet &>(sub);
141 }
142
143 validate_type(type, ns, vm);
144 }
145};
146
149{
150public:
152 : typet(std::move(_id), std::move(_subtype))
153 {
154 }
155
156 const typet &subtype() const
157 {
158 // the existence of get_sub().front() is established by check()
159 return static_cast<const typet &>(get_sub().front());
160 }
161
163 {
164 // the existence of get_sub().front() is established by check()
165 return static_cast<typet &>(get_sub().front());
166 }
167
168 static void check(
169 const typet &type,
171 {
173 vm, type.get_sub().size() == 1, "type must have one type parameter");
174 }
175};
176
178{
180 return static_cast<const type_with_subtypet &>(type);
181}
182
184{
186 return static_cast<type_with_subtypet &>(type);
187}
188
191{
192public:
193 typedef std::vector<typet> subtypest;
194
195 type_with_subtypest(const irep_idt &_id, const subtypest &_subtypes)
196 : typet(_id)
197 {
198 subtypes() = _subtypes;
199 }
200
201 type_with_subtypest(const irep_idt &_id, subtypest &&_subtypes) : typet(_id)
202 {
203 subtypes() = std::move(_subtypes);
204 }
205
207 {
208 return (subtypest &)get_sub();
209 }
210
211 const subtypest &subtypes() const
212 {
213 return (const subtypest &)get_sub();
214 }
215
216 void move_to_subtypes(typet &type); // destroys type
217
218 void copy_to_subtypes(const typet &type);
219};
220
222{
223 return static_cast<const type_with_subtypest &>(type);
224}
225
227{
228 return static_cast<type_with_subtypest &>(type);
229}
230
234
235#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:372
const irept & find(const irep_idt &name) const
Definition irep.cpp:106
subt & get_sub()
Definition irep.h:456
irept & add(const irep_idt &name)
Definition irep.cpp:116
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Type with multiple subtypes.
Definition type.h:191
type_with_subtypest(const irep_idt &_id, const subtypest &_subtypes)
Definition type.h:195
void move_to_subtypes(typet &type)
Move the provided type to the subtypes of this type.
Definition type.cpp:25
std::vector< typet > subtypest
Definition type.h:193
type_with_subtypest(const irep_idt &_id, subtypest &&_subtypes)
Definition type.h:201
subtypest & subtypes()
Definition type.h:206
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:211
Type with a single subtype.
Definition type.h:149
typet & subtype()
Definition type.h:162
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition type.h:168
type_with_subtypet(irep_idt _id, typet _subtype)
Definition type.h:151
const typet & subtype() const
Definition type.h:156
The type of an expression, extends irept.
Definition type.h:29
typet & add_type(const irep_idt &name)
Definition type.h:84
typet(irep_idt _id, typet _subtype)
Definition type.h:37
const typet & find_type(const irep_idt &name) const
Definition type.h:89
typet(const irep_idt &_id)
Definition type.h:33
const typet & subtype() const
Definition type.h:48
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:131
source_locationt & add_source_location()
Definition type.h:79
bool has_subtypes() const
Definition type.h:63
typet & subtype()
Definition type.h:55
typet()
Definition type.h:31
const source_locationt & source_location() const
Definition type.h:74
bool has_subtype() const
Definition type.h:66
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:103
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:115
void remove_subtype()
Definition type.h:71
const irept & get_nil_irep()
Definition irep.cpp:20
STL namespace.
const type_with_subtypest & to_type_with_subtypes(const typet &type)
Definition type.h:221
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition type.h:177
typet remove_const(typet type)
Remove const qualifier from type (if any).
Definition type.cpp:32
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
Definition validate.h:22
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