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 add_subtype() = std::move(_subtype);
45 }
46#endif
47
48 // This method allows the construction of a type with a subtype by
49 // starting from a type without subtype. It avoids copying the contents
50 // of the type. The primary use-case are parsers, where a copy could be
51 // too expensive. Consider type_with_subtypet(id, subtype) for other
52 // use-cases.
54 {
55 subt &sub = get_sub();
56 if(sub.empty())
57 sub.resize(1);
58 return static_cast<typet &>(sub.front());
59 }
60
61 bool has_subtypes() const
62 { return !get_sub().empty(); }
63
64 bool has_subtype() const
65 {
66 return get_sub().size() == 1;
67 }
68
70 { get_sub().clear(); }
71
73 {
74 return (const source_locationt &)find(ID_C_source_location);
75 }
76
78 {
79 return static_cast<source_locationt &>(add(ID_C_source_location));
80 }
81
82 typet &add_type(const irep_idt &name)
83 {
84 return static_cast<typet &>(add(name));
85 }
86
87 const typet &find_type(const irep_idt &name) const
88 {
89 return static_cast<const typet &>(find(name));
90 }
91
100 static void
104
113 static void validate(
114 const typet &type,
115 const namespacet &,
117 {
118 check_type(type, vm);
119 }
120
129 static void validate_full(
130 const typet &type,
131 const namespacet &ns,
133 {
134 // check subtypes
135 for(const irept &sub : type.get_sub())
136 {
137 const typet &subtype = static_cast<const typet &>(sub);
138 validate_full_type(subtype, ns, vm);
139 }
140
141 validate_type(type, ns, vm);
142 }
143};
144
147{
148public:
150 : typet(std::move(_id), std::move(_subtype))
151 {
152 }
153
154 const typet &subtype() const
155 {
156 // the existence of get_sub().front() is established by check()
157 return static_cast<const typet &>(get_sub().front());
158 }
159
161 {
162 // the existence of get_sub().front() is established by check()
163 return static_cast<typet &>(get_sub().front());
164 }
165
166 static void check(
167 const typet &type,
169 {
171 vm, type.get_sub().size() == 1, "type must have one type parameter");
172 }
173};
174
176{
178 return static_cast<const type_with_subtypet &>(type);
179}
180
182{
184 return static_cast<type_with_subtypet &>(type);
185}
186
189{
190public:
191 typedef std::vector<typet> subtypest;
192
193 type_with_subtypest(const irep_idt &_id, const subtypest &_subtypes)
194 : typet(_id)
195 {
196 subtypes() = _subtypes;
197 }
198
199 type_with_subtypest(const irep_idt &_id, subtypest &&_subtypes) : typet(_id)
200 {
201 subtypes() = std::move(_subtypes);
202 }
203
205 {
206 return (subtypest &)get_sub();
207 }
208
209 const subtypest &subtypes() const
210 {
211 return (const subtypest &)get_sub();
212 }
213
214 void move_to_subtypes(typet &type); // destroys type
215
216 void copy_to_subtypes(const typet &type);
217};
218
220{
221 return static_cast<const type_with_subtypest &>(type);
222}
223
225{
226 return static_cast<type_with_subtypest &>(type);
227}
228
232
233#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:39
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:101
subt & get_sub()
Definition irep.h:456
irept & add(const irep_idt &name)
Definition irep.cpp:111
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:189
type_with_subtypest(const irep_idt &_id, const subtypest &_subtypes)
Definition type.h:193
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:191
type_with_subtypest(const irep_idt &_id, subtypest &&_subtypes)
Definition type.h:199
subtypest & subtypes()
Definition type.h:204
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:209
Type with a single subtype.
Definition type.h:147
typet & subtype()
Definition type.h:160
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition type.h:166
type_with_subtypet(irep_idt _id, typet _subtype)
Definition type.h:149
const typet & subtype() const
Definition type.h:154
The type of an expression, extends irept.
Definition type.h:29
typet & add_type(const irep_idt &name)
Definition type.h:82
typet(irep_idt _id, typet _subtype)
Definition type.h:37
const typet & find_type(const irep_idt &name) const
Definition type.h:87
typet(const irep_idt &_id)
Definition type.h:33
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:129
source_locationt & add_source_location()
Definition type.h:77
bool has_subtypes() const
Definition type.h:61
typet()
Definition type.h:31
const source_locationt & source_location() const
Definition type.h:72
bool has_subtype() const
Definition type.h:64
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:101
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:113
void remove_subtype()
Definition type.h:69
typet & add_subtype()
Definition type.h:53
STL namespace.
const type_with_subtypest & to_type_with_subtypes(const typet &type)
Definition type.h:219
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition type.h:175
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