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 #include "invariant.h"
13 
14 #include "c_types.h"
15 
17 {
18  // same as signed size type
19  return signed_size_type();
20 }
21 
24 {
25  // usually same as 'int',
26  // but might be unsigned, or shorter than 'int'
27  return signed_int_type();
28 }
29 
31 {
33  result.set(ID_C_c_type, ID_signed_int);
34  return result;
35 }
36 
38 {
40  result.set(ID_C_c_type, ID_signed_short_int);
41  return result;
42 }
43 
45 {
47  result.set(ID_C_c_type, ID_unsigned_int);
48  return result;
49 }
50 
52 {
54  result.set(ID_C_c_type, ID_unsigned_short_int);
55  return result;
56 }
57 
59 {
60  // The size type varies. This is unsigned int on some systems,
61  // and unsigned long int on others,
62  // and unsigned long long on say Windows 64.
63 
65  return unsigned_int_type();
67  return unsigned_long_int_type();
70  else
71  INVARIANT(false, "width of size type"); // aaah!
72 }
73 
75 {
76  // we presume this is the same as pointer difference
77  return pointer_diff_type();
78 }
79 
81 {
83  result.set(ID_C_c_type, ID_signed_long_int);
84  return result;
85 }
86 
88 {
90  result.set(ID_C_c_type, ID_signed_long_long_int);
91  return result;
92 }
93 
95 {
97  result.set(ID_C_c_type, ID_unsigned_long_int);
98  return result;
99 }
100 
102 {
104  result.set(ID_C_c_type, ID_unsigned_long_long_int);
105  return result;
106 }
107 
109 {
111  return result;
112 }
113 
115 {
116  // this can be signed or unsigned, depending on the architecture
117 
118  // There are 3 char types, i.e., this one is
119  // different from either signed char or unsigned char!
120 
122  {
124  result.set(ID_C_c_type, ID_char);
125  return std::move(result);
126  }
127  else
128  {
130  result.set(ID_C_c_type, ID_char);
131  return std::move(result);
132  }
133 }
134 
136 {
138  result.set(ID_C_c_type, ID_unsigned_char);
139  return result;
140 }
141 
143 {
145  result.set(ID_C_c_type, ID_signed_char);
146  return result;
147 }
148 
150 {
152  {
154  result.set(ID_C_c_type, ID_wchar_t);
155  return std::move(result);
156  }
157  else
158  {
160  result.set(ID_C_c_type, ID_wchar_t);
161  return std::move(result);
162  }
163 }
164 
166 {
167  // Types char16_t and char32_t denote distinct types with the same size,
168  // signedness, and alignment as uint_least16_t and uint_least32_t,
169  // respectively, in <stdint.h>, called the underlying types.
170  unsignedbv_typet result(16);
171  result.set(ID_C_c_type, ID_char16_t);
172  return result;
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(32);
181  result.set(ID_C_c_type, ID_char32_t);
182  return result;
183 }
184 
186 {
187  floatbv_typet result=
189  result.set(ID_C_c_type, ID_float);
190  return result;
191 }
192 
194 {
195  floatbv_typet result=
197  result.set(ID_C_c_type, ID_double);
198  return result;
199 }
200 
202 {
203  floatbv_typet result;
206  else if(config.ansi_c.long_double_width==64)
208  else if(config.ansi_c.long_double_width==80)
209  {
210  // x86 extended precision has 80 bits in total, and
211  // deviating from IEEE, does not use a hidden bit.
212  // We use the closest we have got, but the below isn't accurate.
213  result=ieee_float_spect(63, 15).to_type();
214  }
215  else if(config.ansi_c.long_double_width==96)
216  {
217  result=ieee_float_spect(80, 15).to_type();
218  // not quite right. The extra bits beyond 80 are usually padded.
219  }
220  else
221  INVARIANT(false, "width of long double");
222 
223  result.set(ID_C_c_type, ID_long_double);
224 
225  return result;
226 }
227 
229 {
230  // The pointer-diff type varies. This is signed int on some systems,
231  // and signed long int on others, and signed long long on say Windows.
232 
234  return signed_int_type();
236  return signed_long_int_type();
238  return signed_long_long_int_type();
239  else
240  INVARIANT(false, "width of pointer difference");
241 }
242 
244 {
245  return pointer_typet(subtype, config.ansi_c.pointer_width);
246 }
247 
249 {
250  return reference_typet(subtype, config.ansi_c.pointer_width);
251 }
252 
254 {
255  return empty_typet();
256 }
257 
258 std::string c_type_as_string(const irep_idt &c_type)
259 {
260  if(c_type==ID_signed_int)
261  return "signed int";
262  else if(c_type==ID_signed_short_int)
263  return "signed short int";
264  else if(c_type==ID_unsigned_int)
265  return "unsigned int";
266  else if(c_type==ID_unsigned_short_int)
267  return "unsigned short int";
268  else if(c_type==ID_signed_long_int)
269  return "signed long int";
270  else if(c_type==ID_signed_long_long_int)
271  return "signed long long int";
272  else if(c_type==ID_unsigned_long_int)
273  return "unsigned long int";
274  else if(c_type==ID_unsigned_long_long_int)
275  return "unsigned long long int";
276  else if(c_type==ID_bool)
277  return "_Bool";
278  else if(c_type==ID_char)
279  return "char";
280  else if(c_type==ID_unsigned_char)
281  return "unsigned char";
282  else if(c_type==ID_signed_char)
283  return "signed char";
284  else if(c_type==ID_wchar_t)
285  return "wchar_t";
286  else if(c_type==ID_char16_t)
287  return "char16_t";
288  else if(c_type==ID_char32_t)
289  return "char32_t";
290  else if(c_type==ID_float)
291  return "float";
292  else if(c_type==ID_double)
293  return "double";
294  else if(c_type==ID_long_double)
295  return "long double";
296  else if(c_type==ID_gcc_float128)
297  return "__float128";
298  else if(c_type==ID_unsigned_int128)
299  return "unsigned __int128";
300  else if(c_type==ID_signed_int128)
301  return "signed __int128";
302  else
303  return "";
304 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
configt::ansi_ct::bool_width
std::size_t bool_width
Definition: config.h:32
configt::ansi_ct::wchar_t_width
std::size_t wchar_t_width
Definition: config.h:40
signed_char_type
signedbv_typet signed_char_type()
Definition: c_types.cpp:142
signed_long_long_int_type
signedbv_typet signed_long_long_int_type()
Definition: c_types.cpp:87
reference_typet
The reference type.
Definition: std_types.h:1565
typet
The type of an expression, extends irept.
Definition: type.h:27
char32_t_type
unsignedbv_typet char32_t_type()
Definition: c_types.cpp:175
long_double_type
floatbv_typet long_double_type()
Definition: c_types.cpp:201
floatbv_typet
Fixed-width bit-vector with IEEE floating-point interpretation.
Definition: std_types.h:1398
c_bool_type
typet c_bool_type()
Definition: c_types.cpp:108
ieee_float_spect::quadruple_precision
static ieee_float_spect quadruple_precision()
Definition: ieee_float.h:86
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:400
invariant.h
configt::ansi_c
struct configt::ansi_ct ansi_c
unsigned_char_type
unsignedbv_typet unsigned_char_type()
Definition: c_types.cpp:135
char16_t_type
unsignedbv_typet char16_t_type()
Definition: c_types.cpp:165
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
unsigned_short_int_type
unsignedbv_typet unsigned_short_int_type()
Definition: c_types.cpp:51
unsignedbv_typet
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1223
ieee_float_spect
Definition: ieee_float.h:25
unsigned_long_long_int_type
unsignedbv_typet unsigned_long_long_int_type()
Definition: c_types.cpp:101
configt::ansi_ct::char_width
std::size_t char_width
Definition: config.h:33
enum_constant_type
bitvector_typet enum_constant_type()
return type of enum constants
Definition: c_types.cpp:23
unsigned_long_int_type
unsignedbv_typet unsigned_long_int_type()
Definition: c_types.cpp:94
c_bool_typet
The C/C++ Booleans.
Definition: std_types.h:1611
ieee_float_spect::double_precision
static ieee_float_spect double_precision()
Definition: ieee_float.h:80
empty_typet
The empty type.
Definition: std_types.h:48
signed_int_type
signedbv_typet signed_int_type()
Definition: c_types.cpp:30
configt::ansi_ct::wchar_t_is_unsigned
bool wchar_t_is_unsigned
Definition: config.h:43
ieee_float_spect::to_type
class floatbv_typet to_type() const
Definition: ieee_float.cpp:26
signedbv_typet
Fixed-width bit-vector with two's complement interpretation.
Definition: std_types.h:1278
wchar_t_type
bitvector_typet wchar_t_type()
Definition: c_types.cpp:149
std_types.h
signed_short_int_type
signedbv_typet signed_short_int_type()
Definition: c_types.cpp:37
float_type
floatbv_typet float_type()
Definition: c_types.cpp:185
signed_size_type
signedbv_typet signed_size_type()
Definition: c_types.cpp:74
configt::ansi_ct::long_long_int_width
std::size_t long_long_int_width
Definition: config.h:35
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
unsigned_int_type
unsignedbv_typet unsigned_int_type()
Definition: c_types.cpp:44
double_type
floatbv_typet double_type()
Definition: c_types.cpp:193
config
configt config
Definition: config.cpp:24
char_type
bitvector_typet char_type()
Definition: c_types.cpp:114
reference_type
reference_typet reference_type(const typet &subtype)
Definition: c_types.cpp:248
c_type_as_string
std::string c_type_as_string(const irep_idt &c_type)
Definition: c_types.cpp:258
bitvector_typet
Base class of fixed-width bit-vector types.
Definition: std_types.h:1105
void_type
typet void_type()
Definition: c_types.cpp:253
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
configt::ansi_ct::long_double_width
std::size_t long_double_width
Definition: config.h:39
config.h
configt::ansi_ct::short_int_width
std::size_t short_int_width
Definition: config.h:34
signed_long_int_type
signedbv_typet signed_long_int_type()
Definition: c_types.cpp:80
configt::ansi_ct::char_is_unsigned
bool char_is_unsigned
Definition: config.h:43
configt::ansi_ct::pointer_width
std::size_t pointer_width
Definition: config.h:36
pointer_diff_type
signedbv_typet pointer_diff_type()
Definition: c_types.cpp:228
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1507
size_type
unsignedbv_typet size_type()
Definition: c_types.cpp:58
ieee_float_spect::single_precision
static ieee_float_spect single_precision()
Definition: ieee_float.h:74
configt::ansi_ct::int_width
std::size_t int_width
Definition: config.h:30
c_types.h
configt::ansi_ct::long_int_width
std::size_t long_int_width
Definition: config.h:31