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  static const auto result = empty_typet();
256  return result;
257 }
258 
259 std::string c_type_as_string(const irep_idt &c_type)
260 {
261  if(c_type==ID_signed_int)
262  return "signed int";
263  else if(c_type==ID_signed_short_int)
264  return "signed short int";
265  else if(c_type==ID_unsigned_int)
266  return "unsigned int";
267  else if(c_type==ID_unsigned_short_int)
268  return "unsigned short int";
269  else if(c_type==ID_signed_long_int)
270  return "signed long int";
271  else if(c_type==ID_signed_long_long_int)
272  return "signed long long int";
273  else if(c_type==ID_unsigned_long_int)
274  return "unsigned long int";
275  else if(c_type==ID_unsigned_long_long_int)
276  return "unsigned long long int";
277  else if(c_type==ID_bool)
278  return "_Bool";
279  else if(c_type==ID_char)
280  return "char";
281  else if(c_type==ID_unsigned_char)
282  return "unsigned char";
283  else if(c_type==ID_signed_char)
284  return "signed char";
285  else if(c_type==ID_wchar_t)
286  return "wchar_t";
287  else if(c_type==ID_char16_t)
288  return "char16_t";
289  else if(c_type==ID_char32_t)
290  return "char32_t";
291  else if(c_type==ID_float)
292  return "float";
293  else if(c_type==ID_double)
294  return "double";
295  else if(c_type==ID_long_double)
296  return "long double";
297  else if(c_type==ID_gcc_float128)
298  return "__float128";
299  else if(c_type==ID_unsigned_int128)
300  return "unsigned __int128";
301  else if(c_type==ID_signed_int128)
302  return "signed __int128";
303  else
304  return "";
305 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:36
configt::ansi_ct::bool_width
std::size_t bool_width
Definition: config.h:33
configt::ansi_ct::wchar_t_width
std::size_t wchar_t_width
Definition: config.h:41
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:1552
typet
The type of an expression, extends irept.
Definition: type.h:28
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:1378
c_bool_type
typet c_bool_type()
Definition: c_types.cpp:108
invariant.h
ieee_float_spect::quadruple_precision
static ieee_float_spect quadruple_precision()
Definition: ieee_float.h:86
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
void_type
empty_typet void_type()
Definition: c_types.cpp:253
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:1215
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:34
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:1603
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:45
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:44
ieee_float_spect::to_type
class floatbv_typet to_type() const
Definition: ieee_float.cpp:25
signedbv_typet
Fixed-width bit-vector with two's complement interpretation.
Definition: std_types.h:1264
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:36
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:259
bitvector_typet
Base class of fixed-width bit-vector types.
Definition: std_types.h:1029
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:442
configt::ansi_ct::long_double_width
std::size_t long_double_width
Definition: config.h:40
config.h
configt::ansi_ct::short_int_width
std::size_t short_int_width
Definition: config.h:35
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:44
configt::ansi_ct::pointer_width
std::size_t pointer_width
Definition: config.h:37
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
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:1487
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:31
c_types.h
configt::ansi_ct::long_int_width
std::size_t long_int_width
Definition: config.h:32