cprover
Loading...
Searching...
No Matches
c_types.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "c_types.h"
10
11#include "config.h"
12#include "invariant.h"
13#include "pointer_offset_size.h"
14#include "std_types.h"
15
17{
18 // same as signed size type
19 return signed_size_type();
20}
21
23{
24 return c_index_type();
25}
26
29{
30 // usually same as 'int',
31 // but might be unsigned, or shorter than 'int'
32 return signed_int_type();
33}
34
36{
37 return c_enum_constant_type();
38}
39
41{
43 result.set(ID_C_c_type, ID_signed_int);
44 return result;
45}
46
48{
50 result.set(ID_C_c_type, ID_signed_short_int);
51 return result;
52}
53
55{
57 result.set(ID_C_c_type, ID_unsigned_int);
58 return result;
59}
60
62{
64 result.set(ID_C_c_type, ID_unsigned_short_int);
65 return result;
66}
67
69{
70 // The size type varies. This is unsigned int on some systems,
71 // and unsigned long int on others,
72 // and unsigned long long on say Windows 64.
73
75 return unsigned_int_type();
80 else
81 INVARIANT(false, "width of size type"); // aaah!
82}
83
85{
86 // we presume this is the same as pointer difference
87 return pointer_diff_type();
88}
89
91{
93 result.set(ID_C_c_type, ID_signed_long_int);
94 return result;
95}
96
98{
100 result.set(ID_C_c_type, ID_signed_long_long_int);
101 return result;
102}
103
105{
107 result.set(ID_C_c_type, ID_unsigned_long_int);
108 return result;
109}
110
112{
114 result.set(ID_C_c_type, ID_unsigned_long_long_int);
115 return result;
116}
117
119{
121 return result;
122}
123
125{
126 // this can be signed or unsigned, depending on the architecture
127
128 // There are 3 char types, i.e., this one is
129 // different from either signed char or unsigned char!
130
132 {
134 result.set(ID_C_c_type, ID_char);
135 return std::move(result);
136 }
137 else
138 {
140 result.set(ID_C_c_type, ID_char);
141 return std::move(result);
142 }
143}
144
146{
148 result.set(ID_C_c_type, ID_unsigned_char);
149 return result;
150}
151
153{
155 result.set(ID_C_c_type, ID_signed_char);
156 return result;
157}
158
160{
162 {
164 result.set(ID_C_c_type, ID_wchar_t);
165 return std::move(result);
166 }
167 else
168 {
170 result.set(ID_C_c_type, ID_wchar_t);
171 return std::move(result);
172 }
173}
174
176{
177 // Types char16_t and char32_t denote distinct types with the same size,
178 // signedness, and alignment as uint_least16_t and uint_least32_t,
179 // respectively, in <stdint.h>, called the underlying types.
180 unsignedbv_typet result(16);
181 result.set(ID_C_c_type, ID_char16_t);
182 return result;
183}
184
186{
187 // Types char16_t and char32_t denote distinct types with the same size,
188 // signedness, and alignment as uint_least16_t and uint_least32_t,
189 // respectively, in <stdint.h>, called the underlying types.
190 unsignedbv_typet result(32);
191 result.set(ID_C_c_type, ID_char32_t);
192 return result;
193}
194
196{
197 floatbv_typet result=
199 result.set(ID_C_c_type, ID_float);
200 return result;
201}
202
204{
205 floatbv_typet result=
207 result.set(ID_C_c_type, ID_double);
208 return result;
209}
210
212{
213 floatbv_typet result;
216 else if(config.ansi_c.long_double_width==64)
218 else if(config.ansi_c.long_double_width==80)
219 {
220 // x86 extended precision has 80 bits in total, and
221 // deviating from IEEE, does not use a hidden bit.
222 // We use the closest we have got, but the below isn't accurate.
223 result=ieee_float_spect(63, 15).to_type();
224 }
225 else if(config.ansi_c.long_double_width==96)
226 {
227 result=ieee_float_spect(80, 15).to_type();
228 // not quite right. The extra bits beyond 80 are usually padded.
229 }
230 else
231 INVARIANT(false, "width of long double");
232
233 result.set(ID_C_c_type, ID_long_double);
234
235 return result;
236}
237
239{
240 // The pointer-diff type varies. This is signed int on some systems,
241 // and signed long int on others, and signed long long on say Windows.
242
244 return signed_int_type();
246 return signed_long_int_type();
249 else
250 INVARIANT(false, "width of pointer difference");
251}
252
254{
255 return pointer_typet(subtype, config.ansi_c.pointer_width);
256}
257
259{
261}
262
264{
265 static const auto result = empty_typet();
266 return result;
267}
268
269std::string c_type_as_string(const irep_idt &c_type)
270{
271 if(c_type==ID_signed_int)
272 return "signed int";
273 else if(c_type==ID_signed_short_int)
274 return "signed short int";
275 else if(c_type==ID_unsigned_int)
276 return "unsigned int";
277 else if(c_type==ID_unsigned_short_int)
278 return "unsigned short int";
279 else if(c_type==ID_signed_long_int)
280 return "signed long int";
281 else if(c_type==ID_signed_long_long_int)
282 return "signed long long int";
283 else if(c_type==ID_unsigned_long_int)
284 return "unsigned long int";
285 else if(c_type==ID_unsigned_long_long_int)
286 return "unsigned long long int";
287 else if(c_type==ID_bool)
288 return "_Bool";
289 else if(c_type==ID_char)
290 return "char";
291 else if(c_type==ID_unsigned_char)
292 return "unsigned char";
293 else if(c_type==ID_signed_char)
294 return "signed char";
295 else if(c_type==ID_wchar_t)
296 return "wchar_t";
297 else if(c_type==ID_char16_t)
298 return "char16_t";
299 else if(c_type==ID_char32_t)
300 return "char32_t";
301 else if(c_type==ID_float)
302 return "float";
303 else if(c_type==ID_double)
304 return "double";
305 else if(c_type==ID_long_double)
306 return "long double";
307 else if(c_type==ID_gcc_float128)
308 return "__float128";
309 else if(c_type==ID_unsigned_int128)
310 return "unsigned __int128";
311 else if(c_type==ID_signed_int128)
312 return "signed __int128";
313 else
314 return "";
315}
316
319{
320 const union_typet::componentst &comps = components();
321
322 optionalt<mp_integer> max_width;
323 typet max_comp_type;
324 irep_idt max_comp_name;
325
326 for(const auto &comp : comps)
327 {
328 auto element_width = pointer_offset_bits(comp.type(), ns);
329
330 if(!element_width.has_value())
331 return {};
332
333 if(max_width.has_value() && *element_width <= *max_width)
334 continue;
335
336 max_width = *element_width;
337 max_comp_type = comp.type();
338 max_comp_name = comp.get_name();
339 }
340
341 if(!max_width.has_value())
342 return {};
343 else
344 return std::make_pair(
345 struct_union_typet::componentt{max_comp_name, max_comp_type}, *max_width);
346}
floatbv_typet float_type()
Definition: c_types.cpp:195
bitvector_typet index_type()
Definition: c_types.cpp:22
signedbv_typet signed_long_int_type()
Definition: c_types.cpp:90
signedbv_typet signed_char_type()
Definition: c_types.cpp:152
unsignedbv_typet unsigned_int_type()
Definition: c_types.cpp:54
unsignedbv_typet unsigned_long_long_int_type()
Definition: c_types.cpp:111
unsignedbv_typet char32_t_type()
Definition: c_types.cpp:185
bitvector_typet c_enum_constant_type()
return type of enum constants
Definition: c_types.cpp:28
unsignedbv_typet unsigned_long_int_type()
Definition: c_types.cpp:104
reference_typet reference_type(const typet &subtype)
Definition: c_types.cpp:258
unsignedbv_typet size_type()
Definition: c_types.cpp:68
std::string c_type_as_string(const irep_idt &c_type)
Definition: c_types.cpp:269
empty_typet void_type()
Definition: c_types.cpp:263
signedbv_typet signed_int_type()
Definition: c_types.cpp:40
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:253
signedbv_typet pointer_diff_type()
Definition: c_types.cpp:238
unsignedbv_typet unsigned_char_type()
Definition: c_types.cpp:145
signedbv_typet signed_size_type()
Definition: c_types.cpp:84
bitvector_typet char_type()
Definition: c_types.cpp:124
signedbv_typet signed_long_long_int_type()
Definition: c_types.cpp:97
bitvector_typet wchar_t_type()
Definition: c_types.cpp:159
floatbv_typet long_double_type()
Definition: c_types.cpp:211
bitvector_typet enum_constant_type()
Definition: c_types.cpp:35
typet c_bool_type()
Definition: c_types.cpp:118
bitvector_typet c_index_type()
Definition: c_types.cpp:16
floatbv_typet double_type()
Definition: c_types.cpp:203
signedbv_typet signed_short_int_type()
Definition: c_types.cpp:47
unsignedbv_typet unsigned_short_int_type()
Definition: c_types.cpp:61
unsignedbv_typet char16_t_type()
Definition: c_types.cpp:175
Base class of fixed-width bit-vector types.
Definition: std_types.h:853
The C/C++ Booleans.
Definition: c_types.h:75
struct configt::ansi_ct ansi_c
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
The empty type.
Definition: std_types.h:51
Fixed-width bit-vector with IEEE floating-point interpretation.
static ieee_float_spect single_precision()
Definition: ieee_float.h:71
static ieee_float_spect quadruple_precision()
Definition: ieee_float.h:83
class floatbv_typet to_type() const
Definition: ieee_float.cpp:25
static ieee_float_spect double_precision()
Definition: ieee_float.h:77
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:420
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
The reference type.
Definition: pointer_expr.h:107
Fixed-width bit-vector with two's complement interpretation.
const componentst & components() const
Definition: std_types.h:147
std::vector< componentt > componentst
Definition: std_types.h:140
The type of an expression, extends irept.
Definition: type.h:29
optionalt< std::pair< struct_union_typet::componentt, mp_integer > > find_widest_union_component(const namespacet &ns) const
Determine the member of maximum bit width in a union type.
Definition: c_types.cpp:318
Fixed-width bit-vector with unsigned binary interpretation.
configt config
Definition: config.cpp:25
nonstd::optional< T > optionalt
Definition: optional.h:35
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Pointer Logic.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
Pre-defined types.
std::size_t long_double_width
Definition: config.h:118
bool wchar_t_is_unsigned
Definition: config.h:122
std::size_t pointer_width
Definition: config.h:115
std::size_t wchar_t_width
Definition: config.h:119
bool char_is_unsigned
Definition: config.h:122
std::size_t bool_width
Definition: config.h:111
std::size_t long_long_int_width
Definition: config.h:114
std::size_t long_int_width
Definition: config.h:110
std::size_t short_int_width
Definition: config.h:113
std::size_t char_width
Definition: config.h:112
std::size_t int_width
Definition: config.h:109