cprover
c_types.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #include "std_types.h"
11 #include "config.h"
12 
13 #include "c_types.h"
14 
16 {
17  // same as signed size type
18  return signed_size_type();
19 }
20 
23 {
24  // usually same as 'int',
25  // but might be unsigned, or shorter than 'int'
26  return signed_int_type();
27 }
28 
30 {
32  result.set(ID_C_c_type, ID_signed_int);
33  return result;
34 }
35 
37 {
39  result.set(ID_C_c_type, ID_signed_short_int);
40  return result;
41 }
42 
44 {
46  result.set(ID_C_c_type, ID_unsigned_int);
47  return result;
48 }
49 
51 {
53  result.set(ID_C_c_type, ID_unsigned_short_int);
54  return result;
55 }
56 
58 {
59  // The size type varies. This is unsigned int on some systems,
60  // and unsigned long int on others,
61  // and unsigned long long on say Windows 64.
62 
64  return unsigned_int_type();
66  return unsigned_long_int_type();
69  else
70  assert(false); // aaah!
71 }
72 
74 {
75  // we presume this is the same as pointer difference
76  return pointer_diff_type();
77 }
78 
80 {
82  result.set(ID_C_c_type, ID_signed_long_int);
83  return result;
84 }
85 
87 {
89  result.set(ID_C_c_type, ID_signed_long_long_int);
90  return result;
91 }
92 
94 {
96  result.set(ID_C_c_type, ID_unsigned_long_int);
97  return result;
98 }
99 
101 {
103  result.set(ID_C_c_type, ID_unsigned_long_long_int);
104  return result;
105 }
106 
108 {
110  return result;
111 }
112 
114 {
115  // this can be signed or unsigned, depending on the architecture
116 
117  // There are 3 char types, i.e., this one is
118  // different from either signed char or unsigned char!
119 
121  {
123  result.set(ID_C_c_type, ID_char);
124  return result;
125  }
126  else
127  {
129  result.set(ID_C_c_type, ID_char);
130  return result;
131  }
132 }
133 
135 {
137  result.set(ID_C_c_type, ID_unsigned_char);
138  return result;
139 }
140 
142 {
144  result.set(ID_C_c_type, ID_signed_char);
145  return result;
146 }
147 
149 {
151  {
153  result.set(ID_C_c_type, ID_wchar_t);
154  return result;
155  }
156  else
157  {
159  result.set(ID_C_c_type, ID_wchar_t);
160  return result;
161  }
162 }
163 
165 {
166  // Types char16_t and char32_t denote distinct types with the same size,
167  // signedness, and alignment as uint_least16_t and uint_least32_t,
168  // respectively, in <stdint.h>, called the underlying types.
169  unsignedbv_typet result(16);
170  result.set(ID_C_c_type, ID_char16_t);
171  return result;
172 }
173 
175 {
176  // Types char16_t and char32_t denote distinct types with the same size,
177  // signedness, and alignment as uint_least16_t and uint_least32_t,
178  // respectively, in <stdint.h>, called the underlying types.
179  unsignedbv_typet result(32);
180  result.set(ID_C_c_type, ID_char32_t);
181  return result;
182 }
183 
185 {
187  {
188  fixedbv_typet result;
191  result.set(ID_C_c_type, ID_float);
192  return result;
193  }
194  else
195  {
196  floatbv_typet result=
198  result.set(ID_C_c_type, ID_float);
199  return result;
200  }
201 }
202 
204 {
206  {
207  fixedbv_typet result;
210  result.set(ID_C_c_type, ID_double);
211  return result;
212  }
213  else
214  {
215  floatbv_typet result=
217  result.set(ID_C_c_type, ID_double);
218  return result;
219  }
220 }
221 
223 {
225  {
226  fixedbv_typet result;
229  result.set(ID_C_c_type, ID_long_double);
230  return result;
231  }
232  else
233  {
234  floatbv_typet result;
237  else if(config.ansi_c.long_double_width==64)
239  else if(config.ansi_c.long_double_width==80)
240  {
241  // x86 extended precision has 80 bits in total, and
242  // deviating from IEEE, does not use a hidden bit.
243  // We use the closest we have got, but the below isn't accurate.
244  result=ieee_float_spect(63, 15).to_type();
245  }
246  else if(config.ansi_c.long_double_width==96)
247  {
248  result=ieee_float_spect(80, 15).to_type();
249  // not quite right. The extra bits beyond 80 are usually padded.
250  }
251  else
252  assert(false);
253 
254  result.set(ID_C_c_type, ID_long_double);
255 
256  return result;
257  }
258 }
259 
261 {
262  // not same as long double!
263 
265  {
266  fixedbv_typet result;
267  result.set_width(128);
268  result.set_integer_bits(128/2);
269  result.set(ID_C_c_type, ID_gcc_float128);
270  return result;
271  }
272  else
273  {
274  floatbv_typet result=
276  result.set(ID_C_c_type, ID_gcc_float128);
277  return result;
278  }
279 }
280 
282 {
283  // The pointer-diff type varies. This is signed int on some systems,
284  // and signed long int on others, and signed long long on say Windows.
285 
287  return signed_int_type();
289  return signed_long_int_type();
291  return signed_long_long_int_type();
292  else
293  assert(false); // aaah!
294 }
295 
297 {
298  return pointer_typet(subtype);
299 }
300 
302 {
303  return reference_typet(subtype);
304 }
305 
307 {
308  return empty_typet();
309 }
310 
312 {
313  unsignedbv_typet result(128);
314  result.set(ID_C_c_type, ID_unsigned_int128);
315  return result;
316 }
317 
319 {
320  signedbv_typet result(128);
321  result.set(ID_C_c_type, ID_signed_int128);
322  return result;
323 }
324 
325 std::string c_type_as_string(const irep_idt &c_type)
326 {
327  if(c_type==ID_signed_int)
328  return "signed int";
329  else if(c_type==ID_signed_short_int)
330  return "signed short int";
331  else if(c_type==ID_unsigned_int)
332  return "unsigned int";
333  else if(c_type==ID_unsigned_short_int)
334  return "unsigned short int";
335  else if(c_type==ID_signed_long_int)
336  return "signed long int";
337  else if(c_type==ID_signed_long_long_int)
338  return "signed long long int";
339  else if(c_type==ID_unsigned_long_int)
340  return "unsigned long int";
341  else if(c_type==ID_unsigned_long_long_int)
342  return "unsigned long long int";
343  else if(c_type==ID_bool)
344  return "_Bool";
345  else if(c_type==ID_char)
346  return "char";
347  else if(c_type==ID_unsigned_char)
348  return "unsigned char";
349  else if(c_type==ID_signed_char)
350  return "signed char";
351  else if(c_type==ID_wchar_t)
352  return "wchar_t";
353  else if(c_type==ID_char16_t)
354  return "char16_t";
355  else if(c_type==ID_char32_t)
356  return "char32_t";
357  else if(c_type==ID_float)
358  return "float";
359  else if(c_type==ID_double)
360  return "double";
361  else if(c_type==ID_long_double)
362  return "long double";
363  else if(c_type==ID_gcc_float128)
364  return "__float128";
365  else if(c_type==ID_unsigned_int128)
366  return "unsigned __int128";
367  else if(c_type==ID_signed_int128)
368  return "signed __int128";
369  else
370  return "";
371 }
The type of an expression.
Definition: type.h:20
struct configt::ansi_ct ansi_c
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1125
typet void_type()
Definition: c_types.cpp:306
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:296
unsigned int_width
Definition: config.h:30
unsigned single_width
Definition: config.h:37
Fixed-width bit-vector with IEEE floating-point interpretation.
Definition: std_types.h:1255
unsignedbv_typet unsigned_int_type()
Definition: c_types.cpp:43
unsigned short_int_width
Definition: config.h:34
bitvector_typet enum_constant_type()
return type of enum constants
Definition: c_types.cpp:22
unsignedbv_typet char32_t_type()
Definition: c_types.cpp:174
bitvector_typet double_type()
Definition: c_types.cpp:203
unsignedbv_typet size_type()
Definition: c_types.cpp:57
unsigned char_width
Definition: config.h:33
configt config
Definition: config.cpp:21
signedbv_typet pointer_diff_type()
Definition: c_types.cpp:281
signedbv_typet signed_size_type()
Definition: c_types.cpp:73
static ieee_float_spect double_precision()
Definition: ieee_float.h:69
class floatbv_typet to_type() const
Definition: ieee_float.cpp:26
unsigned wchar_t_width
Definition: config.h:40
bitvector_typet float_type()
Definition: c_types.cpp:184
reference_typet reference_type(const typet &subtype)
Definition: c_types.cpp:301
The pointer type.
Definition: std_types.h:1343
static ieee_float_spect quadruple_precision()
Definition: ieee_float.h:75
unsigned long_long_int_width
Definition: config.h:35
The empty type.
Definition: std_types.h:53
Fixed-width bit-vector with two&#39;s complement interpretation.
Definition: std_types.h:1171
void set_integer_bits(std::size_t b)
Definition: std_types.h:1231
static ieee_float_spect single_precision()
Definition: ieee_float.h:63
signedbv_typet signed_long_int_type()
Definition: c_types.cpp:79
bitvector_typet index_type()
Definition: c_types.cpp:15
Fixed-width bit-vector with signed fixed-point interpretation.
Definition: std_types.h:1217
unsignedbv_typet char16_t_type()
Definition: c_types.cpp:164
Base class of bitvector types.
Definition: std_types.h:1003
bool char_is_unsigned
Definition: config.h:43
std::string c_type_as_string(const irep_idt &c_type)
Definition: c_types.cpp:325
bool use_fixed_for_float
Definition: config.h:44
The reference type.
Definition: std_types.h:1394
bitvector_typet long_double_type()
Definition: c_types.cpp:222
signedbv_typet signed_short_int_type()
Definition: c_types.cpp:36
bitvector_typet wchar_t_type()
Definition: c_types.cpp:148
API to type classes.
unsignedbv_typet gcc_unsigned_int128_type()
Definition: c_types.cpp:311
bitvector_typet gcc_float128_type()
Definition: c_types.cpp:260
unsignedbv_typet unsigned_short_int_type()
Definition: c_types.cpp:50
unsigned bool_width
Definition: config.h:32
unsigned long_double_width
Definition: config.h:39
unsigned double_width
Definition: config.h:38
unsignedbv_typet unsigned_long_long_int_type()
Definition: c_types.cpp:100
signedbv_typet signed_int_type()
Definition: c_types.cpp:29
unsignedbv_typet unsigned_char_type()
Definition: c_types.cpp:134
The C/C++ Booleans.
Definition: std_types.h:1450
unsigned long_int_width
Definition: config.h:31
bool wchar_t_is_unsigned
Definition: config.h:43
unsignedbv_typet unsigned_long_int_type()
Definition: c_types.cpp:93
signedbv_typet gcc_signed_int128_type()
Definition: c_types.cpp:318
signedbv_typet signed_long_long_int_type()
Definition: c_types.cpp:86
unsigned pointer_width
Definition: config.h:36
typet c_bool_type()
Definition: c_types.cpp:107
signedbv_typet signed_char_type()
Definition: c_types.cpp:141
bitvector_typet char_type()
Definition: c_types.cpp:113
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
void set_width(std::size_t width)
Definition: std_types.h:1035