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 #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 
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 }
306 
309 {
310  const union_typet::componentst &comps = components();
311 
312  optionalt<mp_integer> max_width;
313  typet max_comp_type;
314  irep_idt max_comp_name;
315 
316  for(const auto &comp : comps)
317  {
318  auto element_width = pointer_offset_bits(comp.type(), ns);
319 
320  if(!element_width.has_value())
321  return {};
322 
323  if(max_width.has_value() && *element_width <= *max_width)
324  continue;
325 
326  max_width = *element_width;
327  max_comp_type = comp.type();
328  max_comp_name = comp.get_name();
329  }
330 
331  if(!max_width.has_value())
332  return {};
333  else
334  return std::make_pair(
335  struct_union_typet::componentt{max_comp_name, max_comp_type}, *max_width);
336 }
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:141
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
pointer_offset_size.h
Pointer Logic.
configt::ansi_ct::bool_width
std::size_t bool_width
Definition: config.h:113
configt::ansi_ct::wchar_t_width
std::size_t wchar_t_width
Definition: config.h:121
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: pointer_expr.h:89
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
union_typet::find_widest_union_component
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:308
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: bitvector_types.h:322
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
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:134
unsigned_char_type
unsignedbv_typet unsigned_char_type()
Definition: c_types.cpp:135
configt::ansi_c
struct configt::ansi_ct ansi_c
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: bitvector_types.h:159
ieee_float_spect
Definition: ieee_float.h:26
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:114
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: c_types.h:62
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
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:124
ieee_float_spect::to_type
class floatbv_typet to_type() const
Definition: ieee_float.cpp:26
pointer_offset_bits
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:100
signedbv_typet
Fixed-width bit-vector with two's complement interpretation.
Definition: bitvector_types.h:208
wchar_t_type
bitvector_typet wchar_t_type()
Definition: c_types.cpp:149
std_types.h
Pre-defined types.
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:116
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
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
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
struct_union_typet::componentt
Definition: std_types.h:63
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:826
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
invariant.h
configt::ansi_ct::long_double_width
std::size_t long_double_width
Definition: config.h:120
config.h
configt::ansi_ct::short_int_width
std::size_t short_int_width
Definition: config.h:115
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:124
configt::ansi_ct::pointer_width
std::size_t pointer_width
Definition: config.h:117
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: pointer_expr.h:24
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:111
c_types.h
configt::ansi_ct::long_int_width
std::size_t long_int_width
Definition: config.h:112