1
1
/* ******************************************************************\
2
2
3
- Module:
3
+ Module: Data structure for a type of an expression
4
4
5
5
Author: Daniel Kroening, [email protected]
6
+ Maria Svorenova, [email protected]
6
7
7
8
\*******************************************************************/
8
9
10
+ // / \file
11
+ // / Data structure for a type of an expression
9
12
10
13
#ifndef CPROVER_UTIL_TYPE_H
11
14
#define CPROVER_UTIL_TYPE_H
17
20
18
21
class namespacet ;
19
22
20
- /* ! \brief The type of an expression
21
- */
23
+ // / The type of an expression, extends irept. Types may have subtypes. This is
24
+ // / modeled with two subs named “subtype” (a single type) and “subtypes”
25
+ // / (a vector of types). The class typet only adds specialized methods
26
+ // / for accessing the subtype information to the interface of irept.
27
+ // / Pre-defined types:
28
+ // / universe - super type
29
+ // / type - another type
30
+ // / predicate - predicate expression (subtype and predicate)
31
+ // / uninterpreted - uninterpreted type with identifier
32
+ // / empty - void
33
+ // / bool - true or false
34
+ // / abstract - abstract super type
35
+ // / struct - with components: each component has name and type,
36
+ // / the ordering matters
37
+ // / rational
38
+ // / real
39
+ // / integer
40
+ // / complex
41
+ // / string
42
+ // / enum - with elements, the ordering does not matter
43
+ // / tuple - with components: each component has type,
44
+ // / the ordering matters
45
+ // / mapping - domain -> range
46
+ // / bv - no interpretation
47
+ // / unsignedbv
48
+ // / signedbv - two's complement
49
+ // / floatbv - IEEE floating point format
50
+ // / code
51
+ // / pointer - for ANSI-C (subtype)
52
+ // / symbol - look in symbol table (identifier)
53
+ // / number - generic number super type
22
54
class typet :public irept
23
55
{
24
56
public:
@@ -90,7 +122,7 @@ class typet:public irept
90
122
{ remove (ID_subtype); }
91
123
#endif
92
124
93
- void move_to_subtypes (typet &type); // destroys expr
125
+ void move_to_subtypes (typet &type);
94
126
95
127
void copy_to_subtypes (const typet &type);
96
128
@@ -115,6 +147,7 @@ class typet:public irept
115
147
}
116
148
};
117
149
150
+ // / Type with a single subtype.
118
151
class type_with_subtypet :public typet
119
152
{
120
153
public:
@@ -136,6 +169,7 @@ class type_with_subtypet:public typet
136
169
#endif
137
170
};
138
171
172
+ // / Type with multiple subtypes.
139
173
class type_with_subtypest :public typet
140
174
{
141
175
public:
@@ -169,43 +203,8 @@ class type_with_subtypest:public typet
169
203
for (typet::subtypest::iterator it=(type).subtypes().begin(); \
170
204
it!=(type).subtypes().end(); ++it)
171
205
172
- /*
173
-
174
- pre-defined types:
175
- universe // super type
176
- type // another type
177
- predicate // predicate expression (subtype and predicate)
178
- uninterpreted // uninterpreted type with identifier
179
- empty // void
180
- bool // true or false
181
- abstract // abstract super type
182
- struct // with components: each component has name and type
183
- // the ordering matters
184
- rational
185
- real
186
- integer
187
- complex
188
- string
189
- enum // with elements
190
- // the ordering does not matter
191
- tuple // with components: each component has type
192
- // the ordering matters
193
- mapping // domain -> range
194
- bv // no interpretation
195
- unsignedbv
196
- signedbv // two's complement
197
- floatbv // IEEE floating point format
198
- code
199
- pointer // for ANSI-C (subtype)
200
- symbol // look in symbol table (identifier)
201
- number // generic number super type
202
-
203
- */
204
-
205
206
bool is_number (const typet &type);
206
- // rational, real, integer, complex, unsignedbv, signedbv, floatbv
207
207
208
- // Is the passed in type const qualified?
209
208
bool is_constant_or_has_constant_components (
210
209
const typet &type,
211
210
const namespacet &ns);
0 commit comments