cprover
ansi_c_convert_type.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: SpecC Language Conversion
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "ansi_c_convert_type.h"
13 
14 #include <cassert>
15 
16 #include <util/c_types.h>
17 #include <util/config.h>
18 #include <util/namespace.h>
19 #include <util/simplify_expr.h>
20 #include <util/arith_tools.h>
21 #include <util/std_types.h>
22 
23 #include "gcc_types.h"
24 
26 {
27  clear();
29  read_rec(type);
30 }
31 
33 {
34  if(type.id()==ID_merged_type)
35  {
36  forall_subtypes(it, type)
37  read_rec(*it);
38  }
39  else if(type.id()==ID_signed)
40  signed_cnt++;
41  else if(type.id()==ID_unsigned)
42  unsigned_cnt++;
43  else if(type.id()==ID_ptr32)
45  else if(type.id()==ID_ptr64)
47  else if(type.id()==ID_volatile)
49  else if(type.id()==ID_asm)
50  {
51  if(type.has_subtype() &&
52  type.subtype().id()==ID_string_constant)
53  c_storage_spec.asm_label=type.subtype().get(ID_value);
54  }
55  else if(type.id()==ID_section &&
56  type.has_subtype() &&
57  type.subtype().id()==ID_string_constant)
58  {
59  c_storage_spec.section=type.subtype().get(ID_value);
60  }
61  else if(type.id()==ID_const)
63  else if(type.id()==ID_restrict)
65  else if(type.id()==ID_atomic)
67  else if(type.id()==ID_atomic_type_specifier)
68  {
69  // this gets turned into the qualifier, uh
71  read_rec(type.subtype());
72  }
73  else if(type.id()==ID_char)
74  char_cnt++;
75  else if(type.id()==ID_int)
76  int_cnt++;
77  else if(type.id()==ID_int8)
78  int8_cnt++;
79  else if(type.id()==ID_int16)
80  int16_cnt++;
81  else if(type.id()==ID_int32)
82  int32_cnt++;
83  else if(type.id()==ID_int64)
84  int64_cnt++;
85  else if(type.id()==ID_gcc_float16)
87  else if(type.id()==ID_gcc_float32)
89  else if(type.id()==ID_gcc_float32x)
91  else if(type.id()==ID_gcc_float64)
93  else if(type.id()==ID_gcc_float64x)
95  else if(type.id()==ID_gcc_float128)
97  else if(type.id()==ID_gcc_float128x)
99  else if(type.id()==ID_gcc_int128)
100  gcc_int128_cnt++;
101  else if(type.id()==ID_gcc_attribute_mode)
102  {
103  gcc_attribute_mode=type;
104  }
105  else if(type.id()==ID_msc_based)
106  {
107  const exprt &as_expr=
108  static_cast<const exprt &>(static_cast<const irept &>(type));
109  assert(as_expr.operands().size()==1);
110  msc_based=as_expr.op0();
111  }
112  else if(type.id()==ID_custom_bv)
113  {
114  bv_cnt++;
115  const exprt &size_expr=
116  static_cast<const exprt &>(type.find(ID_size));
117 
118  bv_width=size_expr;
119  }
120  else if(type.id()==ID_custom_floatbv)
121  {
122  floatbv_cnt++;
123 
124  const exprt &size_expr=
125  static_cast<const exprt &>(type.find(ID_size));
126  const exprt &fsize_expr=
127  static_cast<const exprt &>(type.find(ID_f));
128 
129  bv_width=size_expr;
130  fraction_width=fsize_expr;
131  }
132  else if(type.id()==ID_custom_fixedbv)
133  {
134  fixedbv_cnt++;
135 
136  const exprt &size_expr=
137  static_cast<const exprt &>(type.find(ID_size));
138  const exprt &fsize_expr=
139  static_cast<const exprt &>(type.find(ID_f));
140 
141  bv_width=size_expr;
142  fraction_width=fsize_expr;
143  }
144  else if(type.id()==ID_short)
145  short_cnt++;
146  else if(type.id()==ID_long)
147  long_cnt++;
148  else if(type.id()==ID_double)
149  double_cnt++;
150  else if(type.id()==ID_float)
151  float_cnt++;
152  else if(type.id()==ID_c_bool)
153  c_bool_cnt++;
154  else if(type.id()==ID_proper_bool)
155  proper_bool_cnt++;
156  else if(type.id()==ID_complex)
157  complex_cnt++;
158  else if(type.id()==ID_static)
160  else if(type.id()==ID_thread_local)
162  else if(type.id()==ID_inline)
164  else if(type.id()==ID_extern)
166  else if(type.id()==ID_typedef)
168  else if(type.id()==ID_register)
170  else if(type.id()==ID_weak)
171  c_storage_spec.is_weak=true;
172  else if(type.id() == ID_used)
173  c_storage_spec.is_used = true;
174  else if(type.id()==ID_auto)
175  {
176  // ignore
177  }
178  else if(type.id()==ID_packed)
179  packed=true;
180  else if(type.id()==ID_aligned)
181  {
182  aligned=true;
183 
184  // may come with size or not
185  if(type.find(ID_size).is_nil())
186  alignment=exprt(ID_default);
187  else
188  alignment=static_cast<const exprt &>(type.find(ID_size));
189  }
190  else if(type.id()==ID_transparent_union)
191  {
193  }
194  else if(type.id()==ID_vector)
196  else if(type.id()==ID_void)
197  {
198  // we store 'void' as 'empty'
199  typet tmp=type;
200  tmp.id(ID_empty);
201  other.push_back(tmp);
202  }
203  else if(type.id()==ID_msc_declspec)
204  {
205  const exprt &as_expr=
206  static_cast<const exprt &>(static_cast<const irept &>(type));
207 
208  forall_operands(it, as_expr)
209  {
210  // these are symbols
211  const irep_idt &id=it->get(ID_identifier);
212 
213  if(id==ID_thread)
215  else if(id=="align")
216  {
217  assert(it->operands().size()==1);
218  aligned=true;
219  alignment=it->op0();
220  }
221  }
222  }
223  else if(type.id()==ID_noreturn)
225  else if(type.id()==ID_constructor)
226  constructor=true;
227  else if(type.id()==ID_destructor)
228  destructor=true;
229  else if(type.id()==ID_alias &&
230  type.has_subtype() &&
231  type.subtype().id()==ID_string_constant)
232  {
233  c_storage_spec.alias=type.subtype().get(ID_value);
234  }
235  else if(type.id()==ID_frontend_pointer)
236  {
237  // We turn ID_frontend_pointer to ID_pointer
238  // Pointers have a width, much like integers,
239  // which is added here.
242  const irep_idt typedef_identifier=type.get(ID_C_typedef);
243  if(!typedef_identifier.empty())
244  tmp.set(ID_C_typedef, typedef_identifier);
245  other.push_back(tmp);
246  }
247  else if(type.id()==ID_pointer)
248  {
249  UNREACHABLE;
250  }
251  else
252  other.push_back(type);
253 }
254 
256 {
257  type.clear();
258 
259  // first, do "other"
260 
261  if(!other.empty())
262  {
263  if(double_cnt || float_cnt || signed_cnt ||
267  gcc_float16_cnt ||
272  {
274  error() << "illegal type modifier for defined type" << eom;
275  throw 0;
276  }
277 
278  // asm blocks (cf. regression/ansi-c/asm1) - ignore the asm
279  if(other.size()==2)
280  {
281  if(other.front().id()==ID_asm && other.back().id()==ID_empty)
282  other.pop_front();
283  else if(other.front().id()==ID_empty && other.back().id()==ID_asm)
284  other.pop_back();
285  }
286 
287  if(other.size()!=1)
288  {
290  error() << "illegal combination of defined types" << eom;
291  throw 0;
292  }
293 
294  type.swap(other.front());
295 
296  if(constructor || destructor)
297  {
298  if(constructor && destructor)
299  {
301  error() << "combining constructor and destructor not supported"
302  << eom;
303  throw 0;
304  }
305 
306  typet *type_p=&type;
307  if(type.id()==ID_code)
308  type_p=&(to_code_type(type).return_type());
309 
310  else if(type_p->id()!=ID_empty)
311  {
313  error() << "constructor and destructor required to be type void, "
314  << "found " << type_p->pretty() << eom;
315  throw 0;
316  }
317 
318  type_p->id(constructor ? ID_constructor : ID_destructor);
319  }
320  }
321  else if(constructor || destructor)
322  {
324  error() << "constructor and destructor required to be type void, "
325  << "found " << type.pretty() << eom;
326  throw 0;
327  }
328  else if(gcc_float16_cnt ||
332  {
335  gcc_int128_cnt || bv_cnt ||
336  short_cnt || char_cnt)
337  {
339  error() << "cannot combine integer type with floating-point type" << eom;
340  throw 0;
341  }
342 
343  if(long_cnt+double_cnt+
348  {
350  error() << "conflicting type modifiers" << eom;
351  throw 0;
352  }
353 
354  // _not_ the same as float, double, long double
355  if(gcc_float16_cnt)
356  type=gcc_float16_type();
357  else if(gcc_float32_cnt)
358  type=gcc_float32_type();
359  else if(gcc_float32x_cnt)
360  type=gcc_float32x_type();
361  else if(gcc_float64_cnt)
362  type=gcc_float64_type();
363  else if(gcc_float64x_cnt)
364  type=gcc_float64x_type();
365  else if(gcc_float128_cnt)
366  type=gcc_float128_type();
367  else if(gcc_float128x_cnt)
368  type=gcc_float128x_type();
369  else
370  UNREACHABLE;
371  }
372  else if(double_cnt || float_cnt)
373  {
377  short_cnt || char_cnt)
378  {
380  error() << "cannot combine integer type with floating-point type" << eom;
381  throw 0;
382  }
383 
384  if(double_cnt && float_cnt)
385  {
387  error() << "conflicting type modifiers" << eom;
388  throw 0;
389  }
390 
391  if(long_cnt==0)
392  {
393  if(double_cnt!=0)
394  type=double_type();
395  else
396  type=float_type();
397  }
398  else if(long_cnt==1 || long_cnt==2)
399  {
400  if(double_cnt!=0)
401  type=long_double_type();
402  else
403  {
405  error() << "conflicting type modifiers" << eom;
406  throw 0;
407  }
408  }
409  else
410  {
412  error() << "illegal type modifier for float" << eom;
413  throw 0;
414  }
415  }
416  else if(c_bool_cnt)
417  {
421  char_cnt || long_cnt)
422  {
424  error() << "illegal type modifier for C boolean type" << eom;
425  throw 0;
426  }
427 
428  type=c_bool_type();
429  }
430  else if(proper_bool_cnt)
431  {
435  char_cnt || long_cnt)
436  {
438  error() << "illegal type modifier for proper boolean type" << eom;
439  throw 0;
440  }
441 
442  type.id(ID_bool);
443  }
444  else if(complex_cnt && !char_cnt && !signed_cnt && !unsigned_cnt &&
446  {
447  // the "default" for complex is double
448  type=double_type();
449  }
450  else if(char_cnt)
451  {
452  if(int_cnt || short_cnt || long_cnt ||
455  {
457  error() << "illegal type modifier for char type" << eom;
458  throw 0;
459  }
460 
461  if(signed_cnt && unsigned_cnt)
462  {
464  error() << "conflicting type modifiers" << eom;
465  throw 0;
466  }
467  else if(unsigned_cnt)
468  type=unsigned_char_type();
469  else if(signed_cnt)
470  type=signed_char_type();
471  else
472  type=char_type();
473  }
474  else
475  {
476  // it is integer -- signed or unsigned?
477 
478  bool is_signed=true; // default
479 
480  if(signed_cnt && unsigned_cnt)
481  {
483  error() << "conflicting type modifiers" << eom;
484  throw 0;
485  }
486  else if(unsigned_cnt)
487  is_signed=false;
488  else if(signed_cnt)
489  is_signed=true;
490 
492  {
494  {
496  error() << "conflicting type modifiers" << eom;
497  throw 0;
498  }
499 
500  if(int8_cnt)
501  if(is_signed)
502  type=signed_char_type();
503  else
504  type=unsigned_char_type();
505  else if(int16_cnt)
506  if(is_signed)
507  type=signed_short_int_type();
508  else
510  else if(int32_cnt)
511  if(is_signed)
512  type=signed_int_type();
513  else
514  type=unsigned_int_type();
515  else if(int64_cnt) // Visual Studio: equivalent to long long int
516  if(is_signed)
518  else
520  else
521  UNREACHABLE;
522  }
523  else if(gcc_int128_cnt)
524  {
525  if(is_signed)
526  type=gcc_signed_int128_type();
527  else
529  }
530  else if(bv_cnt)
531  {
532  // explicitly-given expression for width
533  type.id(is_signed?ID_custom_signedbv:ID_custom_unsignedbv);
534  type.set(ID_size, bv_width);
535  }
536  else if(floatbv_cnt)
537  {
538  type.id(ID_custom_floatbv);
539  type.set(ID_size, bv_width);
540  type.set(ID_f, fraction_width);
541  }
542  else if(fixedbv_cnt)
543  {
544  type.id(ID_custom_fixedbv);
545  type.set(ID_size, bv_width);
546  type.set(ID_f, fraction_width);
547  }
548  else if(short_cnt)
549  {
550  if(long_cnt || char_cnt)
551  {
553  error() << "conflicting type modifiers" << eom;
554  throw 0;
555  }
556 
557  if(is_signed)
558  type=signed_short_int_type();
559  else
561  }
562  else if(long_cnt==0)
563  {
564  if(is_signed)
565  type=signed_int_type();
566  else
567  type=unsigned_int_type();
568  }
569  else if(long_cnt==1)
570  {
571  if(is_signed)
572  type=signed_long_int_type();
573  else
574  type=unsigned_long_int_type();
575  }
576  else if(long_cnt==2)
577  {
578  if(is_signed)
580  else
582  }
583  else
584  {
586  error() << "illegal type modifier for integer type" << eom;
587  throw 0;
588  }
589  }
590 
591  if(vector_size.is_not_nil())
592  {
593  vector_typet new_type(type, vector_size);
595  type=new_type;
596  }
597 
598  if(complex_cnt)
599  {
600  // These take more or less arbitrary subtypes.
601  complex_typet new_type;
603  new_type.subtype()=type;
604  type.swap(new_type);
605  }
606 
608  {
609  typet new_type=gcc_attribute_mode;
610  new_type.subtype()=type;
611  type.swap(new_type);
612  }
613 
614  c_qualifiers.write(type);
615 
616  if(packed)
617  type.set(ID_C_packed, true);
618 
619  if(aligned)
620  type.set(ID_C_alignment, alignment);
621 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
typet::subtype
const typet & subtype() const
Definition: type.h:38
ansi_c_convert_typet::int8_cnt
unsigned int8_cnt
Definition: ansi_c_convert_type.h:29
gcc_float32_type
floatbv_typet gcc_float32_type()
Definition: gcc_types.cpp:22
ansi_c_convert_typet::gcc_attribute_mode
typet gcc_attribute_mode
Definition: ansi_c_convert_type.h:39
irept::clear
void clear()
Definition: irep.h:313
vector_typet::size
const exprt & size() const
Definition: std_types.h:1765
arith_tools.h
ansi_c_convert_typet::msc_based
exprt msc_based
Definition: ansi_c_convert_type.h:43
gcc_float64x_type
floatbv_typet gcc_float64x_type()
Definition: gcc_types.cpp:49
signed_long_long_int_type
signedbv_typet signed_long_long_int_type()
Definition: c_types.cpp:87
signed_char_type
signedbv_typet signed_char_type()
Definition: c_types.cpp:142
typet
The type of an expression, extends irept.
Definition: type.h:27
gcc_float16_type
floatbv_typet gcc_float16_type()
Definition: gcc_types.cpp:14
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:640
ansi_c_convert_type.h
gcc_types.h
typet::has_subtype
bool has_subtype() const
Definition: type.h:56
long_double_type
floatbv_typet long_double_type()
Definition: c_types.cpp:201
c_qualifierst::is_ptr64
bool is_ptr64
Definition: c_qualifiers.h:94
ansi_c_convert_typet::gcc_float32x_cnt
unsigned gcc_float32x_cnt
Definition: ansi_c_convert_type.h:29
ansi_c_convert_typet::write
void write(typet &type)
Definition: ansi_c_convert_type.cpp:255
ansi_c_convert_typet::source_location
source_locationt source_location
Definition: ansi_c_convert_type.h:55
is_signed
bool is_signed(const typet &t)
Convenience function – is the type signed?
Definition: util.cpp:45
ansi_c_convert_typet::vector_size
exprt vector_size
Definition: ansi_c_convert_type.h:42
ansi_c_convert_typet::c_qualifiers
c_qualifierst c_qualifiers
Definition: ansi_c_convert_type.h:50
c_bool_type
typet c_bool_type()
Definition: c_types.cpp:108
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:284
c_qualifierst::is_volatile
bool is_volatile
Definition: c_qualifiers.h:91
c_storage_spect::section
irep_idt section
Definition: c_storage_spec.h:52
ansi_c_convert_typet::int_cnt
unsigned int_cnt
Definition: ansi_c_convert_type.h:23
c_storage_spect::is_extern
bool is_extern
Definition: c_storage_spec.h:44
exprt
Base class for all expressions.
Definition: expr.h:54
complex_typet
Complex numbers made of pair of given subtype.
Definition: std_types.h:1807
exprt::op0
exprt & op0()
Definition: expr.h:84
ansi_c_convert_typet::signed_cnt
unsigned signed_cnt
Definition: ansi_c_convert_type.h:23
vector_typet
The vector type.
Definition: std_types.h:1755
configt::ansi_c
struct configt::ansi_ct ansi_c
messaget::eom
static eomt eom
Definition: message.h:284
unsigned_char_type
unsignedbv_typet unsigned_char_type()
Definition: c_types.cpp:135
ansi_c_convert_typet::gcc_float64x_cnt
unsigned gcc_float64x_cnt
Definition: ansi_c_convert_type.h:29
c_storage_spect::is_register
bool is_register
Definition: c_storage_spec.h:44
namespace.h
gcc_float128_type
floatbv_typet gcc_float128_type()
Definition: gcc_types.cpp:58
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
unsigned_short_int_type
unsignedbv_typet unsigned_short_int_type()
Definition: c_types.cpp:51
ansi_c_convert_typet::double_cnt
unsigned double_cnt
Definition: ansi_c_convert_type.h:23
gcc_float64_type
floatbv_typet gcc_float64_type()
Definition: gcc_types.cpp:40
unsigned_long_long_int_type
unsignedbv_typet unsigned_long_long_int_type()
Definition: c_types.cpp:101
ansi_c_convert_typet::fixedbv_cnt
unsigned fixedbv_cnt
Definition: ansi_c_convert_type.h:29
unsigned_long_int_type
unsignedbv_typet unsigned_long_int_type()
Definition: c_types.cpp:94
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:173
ansi_c_convert_typet::int64_cnt
unsigned int64_cnt
Definition: ansi_c_convert_type.h:29
ansi_c_convert_typet::gcc_float64_cnt
unsigned gcc_float64_cnt
Definition: ansi_c_convert_type.h:29
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:982
c_storage_spect::is_inline
bool is_inline
Definition: c_storage_spec.h:44
messaget::error
mstreamt & error() const
Definition: message.h:386
signed_int_type
signedbv_typet signed_int_type()
Definition: c_types.cpp:30
c_qualifierst::is_constant
bool is_constant
Definition: c_qualifiers.h:91
ansi_c_convert_typet::c_bool_cnt
unsigned c_bool_cnt
Definition: ansi_c_convert_type.h:23
ansi_c_convert_typet::gcc_float32_cnt
unsigned gcc_float32_cnt
Definition: ansi_c_convert_type.h:29
ansi_c_convert_typet::gcc_int128_cnt
unsigned gcc_int128_cnt
Definition: ansi_c_convert_type.h:29
messaget::mstreamt::source_location
source_locationt source_location
Definition: message.h:236
ansi_c_convert_typet::int32_cnt
unsigned int32_cnt
Definition: ansi_c_convert_type.h:29
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:20
gcc_signed_int128_type
signedbv_typet gcc_signed_int128_type()
Definition: gcc_types.cpp:83
ansi_c_convert_typet::bv_cnt
unsigned bv_cnt
Definition: ansi_c_convert_type.h:29
typet::source_location
const source_locationt & source_location() const
Definition: type.h:62
ansi_c_convert_typet::char_cnt
unsigned char_cnt
Definition: ansi_c_convert_type.h:23
ansi_c_convert_typet::complex_cnt
unsigned complex_cnt
Definition: ansi_c_convert_type.h:23
ansi_c_convert_typet::proper_bool_cnt
unsigned proper_bool_cnt
Definition: ansi_c_convert_type.h:23
std_types.h
signed_short_int_type
signedbv_typet signed_short_int_type()
Definition: c_types.cpp:37
c_qualifierst::write
virtual void write(typet &src) const override
Definition: c_qualifiers.cpp:89
float_type
floatbv_typet float_type()
Definition: c_types.cpp:185
ansi_c_convert_typet::gcc_float128_cnt
unsigned gcc_float128_cnt
Definition: ansi_c_convert_type.h:29
ansi_c_convert_typet::short_cnt
unsigned short_cnt
Definition: ansi_c_convert_type.h:23
ansi_c_convert_typet::constructor
bool constructor
Definition: ansi_c_convert_type.h:44
ansi_c_convert_typet::gcc_float16_cnt
unsigned gcc_float16_cnt
Definition: ansi_c_convert_type.h:29
c_storage_spect::asm_label
irep_idt asm_label
Definition: c_storage_spec.h:51
ansi_c_convert_typet::aligned
bool aligned
Definition: ansi_c_convert_type.h:41
unsigned_int_type
unsignedbv_typet unsigned_int_type()
Definition: c_types.cpp:44
irept::swap
void swap(irept &irep)
Definition: irep.h:303
irept::is_nil
bool is_nil() const
Definition: irep.h:172
irept::id
const irep_idt & id() const
Definition: irep.h:259
c_storage_spect::alias
irep_idt alias
Definition: c_storage_spec.h:48
dstringt::empty
bool empty() const
Definition: dstring.h:75
c_storage_spect::is_used
bool is_used
Definition: c_storage_spec.h:44
ansi_c_convert_typet::other
std::list< typet > other
Definition: ansi_c_convert_type.h:57
typet::add_source_location
source_locationt & add_source_location()
Definition: type.h:67
ansi_c_convert_typet::bv_width
exprt bv_width
Definition: ansi_c_convert_type.h:42
ansi_c_convert_typet::c_storage_spec
c_storage_spect c_storage_spec
Definition: ansi_c_convert_type.h:47
forall_subtypes
#define forall_subtypes(it, type)
Definition: type.h:216
double_type
floatbv_typet double_type()
Definition: c_types.cpp:193
config
configt config
Definition: config.cpp:24
ansi_c_convert_typet::long_cnt
unsigned long_cnt
Definition: ansi_c_convert_type.h:23
char_type
bitvector_typet char_type()
Definition: c_types.cpp:114
simplify_expr.h
ansi_c_convert_typet::destructor
bool destructor
Definition: ansi_c_convert_type.h:44
ansi_c_convert_typet::floatbv_cnt
unsigned floatbv_cnt
Definition: ansi_c_convert_type.h:29
ansi_c_convert_typet::unsigned_cnt
unsigned unsigned_cnt
Definition: ansi_c_convert_type.h:23
ansi_c_convert_typet::int16_cnt
unsigned int16_cnt
Definition: ansi_c_convert_type.h:29
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
ansi_c_convert_typet::clear
void clear()
Definition: ansi_c_convert_type.h:65
ansi_c_convert_typet::alignment
exprt alignment
Definition: ansi_c_convert_type.h:42
c_qualifierst::is_atomic
bool is_atomic
Definition: c_qualifiers.h:91
c_qualifierst::is_restricted
bool is_restricted
Definition: c_qualifiers.h:91
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
gcc_unsigned_int128_type
unsignedbv_typet gcc_unsigned_int128_type()
Definition: gcc_types.cpp:76
c_storage_spect::is_weak
bool is_weak
Definition: c_storage_spec.h:44
config.h
signed_long_int_type
signedbv_typet signed_long_int_type()
Definition: c_types.cpp:80
to_vector_type
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1793
ansi_c_convert_typet::packed
bool packed
Definition: ansi_c_convert_type.h:41
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:883
ansi_c_convert_typet::gcc_float128x_cnt
unsigned gcc_float128x_cnt
Definition: ansi_c_convert_type.h:29
ansi_c_convert_typet::read
void read(const typet &type)
Definition: ansi_c_convert_type.cpp:25
c_storage_spect::is_thread_local
bool is_thread_local
Definition: c_storage_spec.h:44
c_storage_spect::is_static
bool is_static
Definition: c_storage_spec.h:44
exprt::operands
operandst & operands()
Definition: expr.h:78
configt::ansi_ct::pointer_width
std::size_t pointer_width
Definition: config.h:36
c_qualifierst::is_ptr32
bool is_ptr32
Definition: c_qualifiers.h:94
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1507
c_storage_spect::is_typedef
bool is_typedef
Definition: c_storage_spec.h:44
ansi_c_convert_typet::float_cnt
unsigned float_cnt
Definition: ansi_c_convert_type.h:23
c_qualifierst::is_noreturn
bool is_noreturn
Definition: c_qualifiers.h:91
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:228
c_types.h
gcc_float32x_type
floatbv_typet gcc_float32x_type()
Definition: gcc_types.cpp:31
ansi_c_convert_typet::fraction_width
exprt fraction_width
Definition: ansi_c_convert_type.h:42
ansi_c_convert_typet::read_rec
void read_rec(const typet &type)
Definition: ansi_c_convert_type.cpp:32
c_qualifierst::is_transparent_union
bool is_transparent_union
Definition: c_qualifiers.h:97
gcc_float128x_type
floatbv_typet gcc_float128x_type()
Definition: gcc_types.cpp:67