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/arith_tools.h>
17 #include <util/c_types.h>
18 #include <util/config.h>
19 #include <util/namespace.h>
20 #include <util/simplify_expr.h>
21 #include <util/std_types.h>
22 #include <util/string_constant.h>
23 
24 #include "gcc_types.h"
25 
27 {
28  clear();
30  read_rec(type);
31 }
32 
34 {
35  if(type.id()==ID_merged_type)
36  {
37  forall_subtypes(it, type)
38  read_rec(*it);
39  }
40  else if(type.id()==ID_signed)
41  signed_cnt++;
42  else if(type.id()==ID_unsigned)
43  unsigned_cnt++;
44  else if(type.id()==ID_ptr32)
46  else if(type.id()==ID_ptr64)
48  else if(type.id()==ID_volatile)
50  else if(type.id()==ID_asm)
51  {
52  if(type.has_subtype() &&
53  type.subtype().id()==ID_string_constant)
55  }
56  else if(type.id()==ID_section &&
57  type.has_subtype() &&
58  type.subtype().id()==ID_string_constant)
59  {
61  }
62  else if(type.id()==ID_const)
64  else if(type.id()==ID_restrict)
66  else if(type.id()==ID_atomic)
68  else if(type.id()==ID_atomic_type_specifier)
69  {
70  // this gets turned into the qualifier, uh
72  read_rec(type.subtype());
73  }
74  else if(type.id()==ID_char)
75  char_cnt++;
76  else if(type.id()==ID_int)
77  int_cnt++;
78  else if(type.id()==ID_int8)
79  int8_cnt++;
80  else if(type.id()==ID_int16)
81  int16_cnt++;
82  else if(type.id()==ID_int32)
83  int32_cnt++;
84  else if(type.id()==ID_int64)
85  int64_cnt++;
86  else if(type.id()==ID_gcc_float16)
88  else if(type.id()==ID_gcc_float32)
90  else if(type.id()==ID_gcc_float32x)
92  else if(type.id()==ID_gcc_float64)
94  else if(type.id()==ID_gcc_float64x)
96  else if(type.id()==ID_gcc_float128)
98  else if(type.id()==ID_gcc_float128x)
100  else if(type.id()==ID_gcc_int128)
101  gcc_int128_cnt++;
102  else if(type.id()==ID_gcc_attribute_mode)
103  {
104  gcc_attribute_mode=type;
105  }
106  else if(type.id()==ID_msc_based)
107  {
108  const exprt &as_expr=
109  static_cast<const exprt &>(static_cast<const irept &>(type));
110  msc_based = to_unary_expr(as_expr).op();
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  aligned=true;
218  alignment = to_unary_expr(*it).op();
219  }
220  }
221  }
222  else if(type.id()==ID_noreturn)
224  else if(type.id()==ID_constructor)
225  constructor=true;
226  else if(type.id()==ID_destructor)
227  destructor=true;
228  else if(type.id()==ID_alias &&
229  type.has_subtype() &&
230  type.subtype().id()==ID_string_constant)
231  {
233  }
234  else if(type.id()==ID_frontend_pointer)
235  {
236  // We turn ID_frontend_pointer to ID_pointer
237  // Pointers have a width, much like integers,
238  // which is added here.
241  const irep_idt typedef_identifier=type.get(ID_C_typedef);
242  if(!typedef_identifier.empty())
243  tmp.set(ID_C_typedef, typedef_identifier);
244  other.push_back(tmp);
245  }
246  else if(type.id()==ID_pointer)
247  {
248  UNREACHABLE;
249  }
250  else
251  other.push_back(type);
252 }
253 
255 {
256  type.clear();
257 
258  // first, do "other"
259 
260  if(!other.empty())
261  {
262  if(double_cnt || float_cnt || signed_cnt ||
266  gcc_float16_cnt ||
271  {
273  error() << "illegal type modifier for defined type" << eom;
274  throw 0;
275  }
276 
277  // asm blocks (cf. regression/ansi-c/asm1) - ignore the asm
278  if(other.size()==2)
279  {
280  if(other.front().id()==ID_asm && other.back().id()==ID_empty)
281  other.pop_front();
282  else if(other.front().id()==ID_empty && other.back().id()==ID_asm)
283  other.pop_back();
284  }
285 
286  if(other.size()!=1)
287  {
289  error() << "illegal combination of defined types" << eom;
290  throw 0;
291  }
292 
293  type.swap(other.front());
294 
295  if(constructor || destructor)
296  {
297  if(constructor && destructor)
298  {
300  error() << "combining constructor and destructor not supported"
301  << eom;
302  throw 0;
303  }
304 
305  typet *type_p=&type;
306  if(type.id()==ID_code)
307  type_p=&(to_code_type(type).return_type());
308 
309  else if(type_p->id()!=ID_empty)
310  {
312  error() << "constructor and destructor required to be type void, "
313  << "found " << type_p->pretty() << eom;
314  throw 0;
315  }
316 
317  type_p->id(constructor ? ID_constructor : ID_destructor);
318  }
319  }
320  else if(constructor || destructor)
321  {
323  error() << "constructor and destructor required to be type void, "
324  << "found " << type.pretty() << eom;
325  throw 0;
326  }
327  else if(gcc_float16_cnt ||
331  {
334  gcc_int128_cnt || bv_cnt ||
335  short_cnt || char_cnt)
336  {
338  error() << "cannot combine integer type with floating-point type" << eom;
339  throw 0;
340  }
341 
342  if(long_cnt+double_cnt+
347  {
349  error() << "conflicting type modifiers" << eom;
350  throw 0;
351  }
352 
353  // _not_ the same as float, double, long double
354  if(gcc_float16_cnt)
355  type=gcc_float16_type();
356  else if(gcc_float32_cnt)
357  type=gcc_float32_type();
358  else if(gcc_float32x_cnt)
359  type=gcc_float32x_type();
360  else if(gcc_float64_cnt)
361  type=gcc_float64_type();
362  else if(gcc_float64x_cnt)
363  type=gcc_float64x_type();
364  else if(gcc_float128_cnt)
365  type=gcc_float128_type();
366  else if(gcc_float128x_cnt)
367  type=gcc_float128x_type();
368  else
369  UNREACHABLE;
370  }
371  else if(double_cnt || float_cnt)
372  {
376  short_cnt || char_cnt)
377  {
379  error() << "cannot combine integer type with floating-point type" << eom;
380  throw 0;
381  }
382 
383  if(double_cnt && float_cnt)
384  {
386  error() << "conflicting type modifiers" << eom;
387  throw 0;
388  }
389 
390  if(long_cnt==0)
391  {
392  if(double_cnt!=0)
393  type=double_type();
394  else
395  type=float_type();
396  }
397  else if(long_cnt==1 || long_cnt==2)
398  {
399  if(double_cnt!=0)
400  type=long_double_type();
401  else
402  {
404  error() << "conflicting type modifiers" << eom;
405  throw 0;
406  }
407  }
408  else
409  {
411  error() << "illegal type modifier for float" << eom;
412  throw 0;
413  }
414  }
415  else if(c_bool_cnt)
416  {
420  char_cnt || long_cnt)
421  {
423  error() << "illegal type modifier for C boolean type" << eom;
424  throw 0;
425  }
426 
427  type=c_bool_type();
428  }
429  else if(proper_bool_cnt)
430  {
434  char_cnt || long_cnt)
435  {
437  error() << "illegal type modifier for proper boolean type" << eom;
438  throw 0;
439  }
440 
441  type.id(ID_bool);
442  }
443  else if(complex_cnt && !char_cnt && !signed_cnt && !unsigned_cnt &&
445  {
446  // the "default" for complex is double
447  type=double_type();
448  }
449  else if(char_cnt)
450  {
451  if(int_cnt || short_cnt || long_cnt ||
454  {
456  error() << "illegal type modifier for char type" << eom;
457  throw 0;
458  }
459 
460  if(signed_cnt && unsigned_cnt)
461  {
463  error() << "conflicting type modifiers" << eom;
464  throw 0;
465  }
466  else if(unsigned_cnt)
467  type=unsigned_char_type();
468  else if(signed_cnt)
469  type=signed_char_type();
470  else
471  type=char_type();
472  }
473  else
474  {
475  // it is integer -- signed or unsigned?
476 
477  bool is_signed=true; // default
478 
479  if(signed_cnt && unsigned_cnt)
480  {
482  error() << "conflicting type modifiers" << eom;
483  throw 0;
484  }
485  else if(unsigned_cnt)
486  is_signed=false;
487  else if(signed_cnt)
488  is_signed=true;
489 
491  {
493  {
495  error() << "conflicting type modifiers" << eom;
496  throw 0;
497  }
498 
499  if(int8_cnt)
500  if(is_signed)
501  type=signed_char_type();
502  else
503  type=unsigned_char_type();
504  else if(int16_cnt)
505  if(is_signed)
506  type=signed_short_int_type();
507  else
509  else if(int32_cnt)
510  if(is_signed)
511  type=signed_int_type();
512  else
513  type=unsigned_int_type();
514  else if(int64_cnt) // Visual Studio: equivalent to long long int
515  if(is_signed)
517  else
519  else
520  UNREACHABLE;
521  }
522  else if(gcc_int128_cnt)
523  {
524  if(is_signed)
525  type=gcc_signed_int128_type();
526  else
528  }
529  else if(bv_cnt)
530  {
531  // explicitly-given expression for width
532  type.id(is_signed?ID_custom_signedbv:ID_custom_unsignedbv);
533  type.set(ID_size, bv_width);
534  }
535  else if(floatbv_cnt)
536  {
537  type.id(ID_custom_floatbv);
538  type.set(ID_size, bv_width);
539  type.set(ID_f, fraction_width);
540  }
541  else if(fixedbv_cnt)
542  {
543  type.id(ID_custom_fixedbv);
544  type.set(ID_size, bv_width);
545  type.set(ID_f, fraction_width);
546  }
547  else if(short_cnt)
548  {
549  if(long_cnt || char_cnt)
550  {
552  error() << "conflicting type modifiers" << eom;
553  throw 0;
554  }
555 
556  if(is_signed)
557  type=signed_short_int_type();
558  else
560  }
561  else if(long_cnt==0)
562  {
563  if(is_signed)
564  type=signed_int_type();
565  else
566  type=unsigned_int_type();
567  }
568  else if(long_cnt==1)
569  {
570  if(is_signed)
571  type=signed_long_int_type();
572  else
573  type=unsigned_long_int_type();
574  }
575  else if(long_cnt==2)
576  {
577  if(is_signed)
579  else
581  }
582  else
583  {
585  error() << "illegal type modifier for integer type" << eom;
586  throw 0;
587  }
588  }
589 
591  set_attributes(type);
592 }
593 
596 {
597  if(vector_size.is_not_nil())
598  {
599  type_with_subtypet new_type(ID_frontend_vector, type);
600  new_type.set(ID_size, vector_size);
602  type=new_type;
603  }
604 
605  if(complex_cnt)
606  {
607  // These take more or less arbitrary subtypes.
608  complex_typet new_type(type);
610  type.swap(new_type);
611  }
612 }
613 
616 {
618  {
619  typet new_type=gcc_attribute_mode;
620  new_type.subtype()=type;
621  type.swap(new_type);
622  }
623 
624  c_qualifiers.write(type);
625 
626  if(packed)
627  type.set(ID_C_packed, true);
628 
629  if(aligned)
630  type.set(ID_C_alignment, alignment);
631 }
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
to_unary_expr
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:316
typet::subtype
const typet & subtype() const
Definition: type.h:47
ansi_c_convert_typet::int8_cnt
unsigned int8_cnt
Definition: ansi_c_convert_type.h:31
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:41
irept::clear
void clear()
Definition: irep.h:473
ansi_c_convert_typet::clear
virtual void clear()
Definition: ansi_c_convert_type.h:67
ansi_c_convert_typet::set_attributes
virtual void set_attributes(typet &type) const
Add qualifiers and GCC attributes onto type.
Definition: ansi_c_convert_type.cpp:615
arith_tools.h
ansi_c_convert_typet::msc_based
exprt msc_based
Definition: ansi_c_convert_type.h:45
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:29
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:488
ansi_c_convert_type.h
ANSI-C Language Conversion.
gcc_types.h
typet::has_subtype
bool has_subtype() const
Definition: type.h:65
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:34
ansi_c_convert_typet::write
virtual void write(typet &type)
Definition: ansi_c_convert_type.cpp:254
ansi_c_convert_typet::source_location
source_locationt source_location
Definition: ansi_c_convert_type.h:57
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:44
ansi_c_convert_typet::c_qualifiers
c_qualifierst c_qualifiers
Definition: ansi_c_convert_type.h:52
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:103
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:26
c_storage_spect::is_extern
bool is_extern
Definition: c_storage_spec.h:44
to_string_constant
const string_constantt & to_string_constant(const exprt &expr)
Definition: string_constant.h:31
string_constant.h
exprt
Base class for all expressions.
Definition: expr.h:53
complex_typet
Complex numbers made of pair of given subtype.
Definition: std_types.h:1790
ansi_c_convert_typet::signed_cnt
unsigned signed_cnt
Definition: ansi_c_convert_type.h:25
messaget::eom
static eomt eom
Definition: message.h:297
unsigned_char_type
unsignedbv_typet unsigned_char_type()
Definition: c_types.cpp:135
type_with_subtypet
Type with a single subtype.
Definition: type.h:146
ansi_c_convert_typet::gcc_float64x_cnt
unsigned gcc_float64x_cnt
Definition: ansi_c_convert_type.h:35
c_storage_spect::is_register
bool is_register
Definition: c_storage_spec.h:44
configt::ansi_c
struct configt::ansi_ct ansi_c
namespace.h
gcc_float128_type
floatbv_typet gcc_float128_type()
Definition: gcc_types.cpp:58
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:27
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:39
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:402
ansi_c_convert_typet::int64_cnt
unsigned int64_cnt
Definition: ansi_c_convert_type.h:31
ansi_c_convert_typet::gcc_float64_cnt
unsigned gcc_float64_cnt
Definition: ansi_c_convert_type.h:35
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:946
c_storage_spect::is_inline
bool is_inline
Definition: c_storage_spec.h:45
messaget::error
mstreamt & error() const
Definition: message.h:399
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:27
ansi_c_convert_typet::gcc_float32_cnt
unsigned gcc_float32_cnt
Definition: ansi_c_convert_type.h:34
ansi_c_convert_typet::gcc_int128_cnt
unsigned gcc_int128_cnt
Definition: ansi_c_convert_type.h:37
messaget::mstreamt::source_location
source_locationt source_location
Definition: message.h:247
ansi_c_convert_typet::int32_cnt
unsigned int32_cnt
Definition: ansi_c_convert_type.h:31
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
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:38
typet::source_location
const source_locationt & source_location() const
Definition: type.h:71
ansi_c_convert_typet::char_cnt
unsigned char_cnt
Definition: ansi_c_convert_type.h:25
ansi_c_convert_typet::complex_cnt
unsigned complex_cnt
Definition: ansi_c_convert_type.h:28
ansi_c_convert_typet::proper_bool_cnt
unsigned proper_bool_cnt
Definition: ansi_c_convert_type.h:28
std_types.h
Pre-defined types.
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:36
ansi_c_convert_typet::short_cnt
unsigned short_cnt
Definition: ansi_c_convert_type.h:26
ansi_c_convert_typet::constructor
bool constructor
Definition: ansi_c_convert_type.h:46
ansi_c_convert_typet::gcc_float16_cnt
unsigned gcc_float16_cnt
Definition: ansi_c_convert_type.h:33
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:43
unsigned_int_type
unsignedbv_typet unsigned_int_type()
Definition: c_types.cpp:44
irept::swap
void swap(irept &irep)
Definition: irep.h:463
irept::is_nil
bool is_nil() const
Definition: irep.h:398
irept::id
const irep_idt & id() const
Definition: irep.h:418
c_storage_spect::alias
irep_idt alias
Definition: c_storage_spec.h:48
dstringt::empty
bool empty() const
Definition: dstring.h:88
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:281
c_storage_spect::is_used
bool is_used
Definition: c_storage_spec.h:45
ansi_c_convert_typet::other
std::list< typet > other
Definition: ansi_c_convert_type.h:59
typet::add_source_location
source_locationt & add_source_location()
Definition: type.h:76
ansi_c_convert_typet::bv_width
exprt bv_width
Definition: ansi_c_convert_type.h:44
vector_typet::size
const constant_exprt & size() const
Definition: std_types.cpp:268
ansi_c_convert_typet::c_storage_spec
c_storage_spect c_storage_spec
Definition: ansi_c_convert_type.h:49
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:26
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:46
ansi_c_convert_typet::floatbv_cnt
unsigned floatbv_cnt
Definition: ansi_c_convert_type.h:39
ansi_c_convert_typet::build_type_with_subtype
virtual void build_type_with_subtype(typet &type) const
Build a vector or complex type with type as subtype.
Definition: ansi_c_convert_type.cpp:595
ansi_c_convert_typet::unsigned_cnt
unsigned unsigned_cnt
Definition: ansi_c_convert_type.h:25
ansi_c_convert_typet::int16_cnt
unsigned int16_cnt
Definition: ansi_c_convert_type.h:31
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
ansi_c_convert_typet::alignment
exprt alignment
Definition: ansi_c_convert_type.h:44
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:442
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:45
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:1775
ansi_c_convert_typet::packed
bool packed
Definition: ansi_c_convert_type.h:43
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:847
ansi_c_convert_typet::gcc_float128x_cnt
unsigned gcc_float128x_cnt
Definition: ansi_c_convert_type.h:36
ansi_c_convert_typet::read
virtual void read(const typet &type)
Definition: ansi_c_convert_type.cpp:26
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:394
c_storage_spect::is_thread_local
bool is_thread_local
Definition: c_storage_spec.h:45
c_storage_spect::is_static
bool is_static
Definition: c_storage_spec.h:44
configt::ansi_ct::pointer_width
std::size_t pointer_width
Definition: config.h:37
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:1488
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:27
c_qualifierst::is_noreturn
bool is_noreturn
Definition: c_qualifiers.h:91
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:254
c_types.h
gcc_float32x_type
floatbv_typet gcc_float32x_type()
Definition: gcc_types.cpp:31
string_constantt::get_value
const irep_idt & get_value() const
Definition: string_constant.h:22
ansi_c_convert_typet::fraction_width
exprt fraction_width
Definition: ansi_c_convert_type.h:44
ansi_c_convert_typet::read_rec
virtual void read_rec(const typet &type)
Definition: ansi_c_convert_type.cpp:33
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