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 <util/arith_tools.h>
15 #include <util/c_types.h>
16 #include <util/config.h>
17 #include <util/namespace.h>
18 #include <util/simplify_expr.h>
19 #include <util/std_types.h>
20 #include <util/string_constant.h>
21 
22 #include "gcc_types.h"
23 
25 {
26  clear();
28  read_rec(type);
29 }
30 
32 {
33  if(type.id()==ID_merged_type)
34  {
35  for(const typet &subtype : to_type_with_subtypes(type).subtypes())
36  read_rec(subtype);
37  }
38  else if(type.id()==ID_signed)
39  signed_cnt++;
40  else if(type.id()==ID_unsigned)
41  unsigned_cnt++;
42  else if(type.id()==ID_ptr32)
44  else if(type.id()==ID_ptr64)
46  else if(type.id()==ID_volatile)
48  else if(type.id()==ID_asm)
49  {
50  if(type.has_subtype() &&
51  type.subtype().id()==ID_string_constant)
53  }
54  else if(type.id()==ID_section &&
55  type.has_subtype() &&
56  type.subtype().id()==ID_string_constant)
57  {
59  }
60  else if(type.id()==ID_const)
62  else if(type.id()==ID_restrict)
64  else if(type.id()==ID_atomic)
66  else if(type.id()==ID_atomic_type_specifier)
67  {
68  // this gets turned into the qualifier, uh
70  read_rec(type.subtype());
71  }
72  else if(type.id()==ID_char)
73  char_cnt++;
74  else if(type.id()==ID_int)
75  int_cnt++;
76  else if(type.id()==ID_int8)
77  int8_cnt++;
78  else if(type.id()==ID_int16)
79  int16_cnt++;
80  else if(type.id()==ID_int32)
81  int32_cnt++;
82  else if(type.id()==ID_int64)
83  int64_cnt++;
84  else if(type.id()==ID_gcc_float16)
86  else if(type.id()==ID_gcc_float32)
88  else if(type.id()==ID_gcc_float32x)
90  else if(type.id()==ID_gcc_float64)
92  else if(type.id()==ID_gcc_float64x)
94  else if(type.id()==ID_gcc_float128)
96  else if(type.id()==ID_gcc_float128x)
98  else if(type.id()==ID_gcc_int128)
100  else if(type.id()==ID_gcc_attribute_mode)
101  {
102  gcc_attribute_mode=type;
103  }
104  else if(type.id()==ID_msc_based)
105  {
106  const exprt &as_expr=
107  static_cast<const exprt &>(static_cast<const irept &>(type));
108  msc_based = to_unary_expr(as_expr).op();
109  }
110  else if(type.id()==ID_custom_bv)
111  {
112  bv_cnt++;
113  const exprt &size_expr=
114  static_cast<const exprt &>(type.find(ID_size));
115 
116  bv_width=size_expr;
117  }
118  else if(type.id()==ID_custom_floatbv)
119  {
120  floatbv_cnt++;
121 
122  const exprt &size_expr=
123  static_cast<const exprt &>(type.find(ID_size));
124  const exprt &fsize_expr=
125  static_cast<const exprt &>(type.find(ID_f));
126 
127  bv_width=size_expr;
128  fraction_width=fsize_expr;
129  }
130  else if(type.id()==ID_custom_fixedbv)
131  {
132  fixedbv_cnt++;
133 
134  const exprt &size_expr=
135  static_cast<const exprt &>(type.find(ID_size));
136  const exprt &fsize_expr=
137  static_cast<const exprt &>(type.find(ID_f));
138 
139  bv_width=size_expr;
140  fraction_width=fsize_expr;
141  }
142  else if(type.id()==ID_short)
143  short_cnt++;
144  else if(type.id()==ID_long)
145  long_cnt++;
146  else if(type.id()==ID_double)
147  double_cnt++;
148  else if(type.id()==ID_float)
149  float_cnt++;
150  else if(type.id()==ID_c_bool)
151  c_bool_cnt++;
152  else if(type.id()==ID_proper_bool)
153  proper_bool_cnt++;
154  else if(type.id()==ID_complex)
155  complex_cnt++;
156  else if(type.id()==ID_static)
158  else if(type.id()==ID_thread_local)
160  else if(type.id()==ID_inline)
162  else if(type.id()==ID_extern)
164  else if(type.id()==ID_typedef)
166  else if(type.id()==ID_register)
168  else if(type.id()==ID_weak)
169  c_storage_spec.is_weak=true;
170  else if(type.id() == ID_used)
171  c_storage_spec.is_used = true;
172  else if(type.id()==ID_auto)
173  {
174  // ignore
175  }
176  else if(type.id()==ID_packed)
177  packed=true;
178  else if(type.id()==ID_aligned)
179  {
180  aligned=true;
181 
182  // may come with size or not
183  if(type.find(ID_size).is_nil())
184  alignment=exprt(ID_default);
185  else
186  alignment=static_cast<const exprt &>(type.find(ID_size));
187  }
188  else if(type.id()==ID_transparent_union)
189  {
191  }
192  else if(type.id()==ID_vector)
194  else if(type.id()==ID_void)
195  {
196  // we store 'void' as 'empty'
197  typet tmp=type;
198  tmp.id(ID_empty);
199  other.push_back(tmp);
200  }
201  else if(type.id()==ID_msc_declspec)
202  {
203  const exprt &as_expr=
204  static_cast<const exprt &>(static_cast<const irept &>(type));
205 
206  forall_operands(it, as_expr)
207  {
208  // these are symbols
209  const irep_idt &id=it->get(ID_identifier);
210 
211  if(id==ID_thread)
213  else if(id=="align")
214  {
215  aligned=true;
216  alignment = to_unary_expr(*it).op();
217  }
218  }
219  }
220  else if(type.id()==ID_noreturn)
222  else if(type.id()==ID_constructor)
223  constructor=true;
224  else if(type.id()==ID_destructor)
225  destructor=true;
226  else if(type.id()==ID_alias &&
227  type.has_subtype() &&
228  type.subtype().id()==ID_string_constant)
229  {
231  }
232  else if(type.id()==ID_frontend_pointer)
233  {
234  // We turn ID_frontend_pointer to ID_pointer
235  // Pointers have a width, much like integers,
236  // which is added here.
239  const irep_idt typedef_identifier=type.get(ID_C_typedef);
240  if(!typedef_identifier.empty())
241  tmp.set(ID_C_typedef, typedef_identifier);
242  other.push_back(tmp);
243  }
244  else if(type.id()==ID_pointer)
245  {
246  UNREACHABLE;
247  }
248  else if(type.id() == ID_C_spec_requires)
249  {
250  const exprt &as_expr =
251  static_cast<const exprt &>(static_cast<const irept &>(type));
252  requires = to_unary_expr(as_expr).op();
253  }
254  else if(type.id() == ID_C_spec_assigns)
255  {
256  const exprt &as_expr =
257  static_cast<const exprt &>(static_cast<const irept &>(type));
258  assigns = to_unary_expr(as_expr).op();
259  }
260  else if(type.id() == ID_C_spec_ensures)
261  {
262  const exprt &as_expr =
263  static_cast<const exprt &>(static_cast<const irept &>(type));
264  ensures = to_unary_expr(as_expr).op();
265  }
266  else
267  other.push_back(type);
268 }
269 
271 {
272  type.clear();
273 
274  // first, do "other"
275 
276  if(!other.empty())
277  {
278  if(double_cnt || float_cnt || signed_cnt ||
282  gcc_float16_cnt ||
287  {
289  error() << "illegal type modifier for defined type" << eom;
290  throw 0;
291  }
292 
293  // asm blocks (cf. regression/ansi-c/asm1) - ignore the asm
294  if(other.size()==2)
295  {
296  if(other.front().id()==ID_asm && other.back().id()==ID_empty)
297  other.pop_front();
298  else if(other.front().id()==ID_empty && other.back().id()==ID_asm)
299  other.pop_back();
300  }
301 
302  if(other.size()!=1)
303  {
305  error() << "illegal combination of defined types" << eom;
306  throw 0;
307  }
308 
309  type.swap(other.front());
310 
311  // the contract expressions are meant for function types only
312  if(requires.is_not_nil())
313  type.add(ID_C_spec_requires) = std::move(requires);
314 
315  if(assigns.is_not_nil())
316  type.add(ID_C_spec_assigns) = std::move(assigns);
317 
318  if(ensures.is_not_nil())
319  type.add(ID_C_spec_ensures) = std::move(ensures);
320 
321  if(constructor || destructor)
322  {
323  if(constructor && destructor)
324  {
326  error() << "combining constructor and destructor not supported"
327  << eom;
328  throw 0;
329  }
330 
331  typet *type_p=&type;
332  if(type.id()==ID_code)
333  type_p=&(to_code_type(type).return_type());
334 
335  else if(type_p->id()!=ID_empty)
336  {
338  error() << "constructor and destructor required to be type void, "
339  << "found " << type_p->pretty() << eom;
340  throw 0;
341  }
342 
343  type_p->id(constructor ? ID_constructor : ID_destructor);
344  }
345  }
346  else if(constructor || destructor)
347  {
349  error() << "constructor and destructor required to be type void, "
350  << "found " << type.pretty() << eom;
351  throw 0;
352  }
353  else if(gcc_float16_cnt ||
357  {
360  gcc_int128_cnt || bv_cnt ||
361  short_cnt || char_cnt)
362  {
364  error() << "cannot combine integer type with floating-point type" << eom;
365  throw 0;
366  }
367 
368  if(long_cnt+double_cnt+
373  {
375  error() << "conflicting type modifiers" << eom;
376  throw 0;
377  }
378 
379  // _not_ the same as float, double, long double
380  if(gcc_float16_cnt)
381  type=gcc_float16_type();
382  else if(gcc_float32_cnt)
383  type=gcc_float32_type();
384  else if(gcc_float32x_cnt)
385  type=gcc_float32x_type();
386  else if(gcc_float64_cnt)
387  type=gcc_float64_type();
388  else if(gcc_float64x_cnt)
389  type=gcc_float64x_type();
390  else if(gcc_float128_cnt)
391  type=gcc_float128_type();
392  else if(gcc_float128x_cnt)
393  type=gcc_float128x_type();
394  else
395  UNREACHABLE;
396  }
397  else if(double_cnt || float_cnt)
398  {
402  short_cnt || char_cnt)
403  {
405  error() << "cannot combine integer type with floating-point type" << eom;
406  throw 0;
407  }
408 
409  if(double_cnt && float_cnt)
410  {
412  error() << "conflicting type modifiers" << eom;
413  throw 0;
414  }
415 
416  if(long_cnt==0)
417  {
418  if(double_cnt!=0)
419  type=double_type();
420  else
421  type=float_type();
422  }
423  else if(long_cnt==1 || long_cnt==2)
424  {
425  if(double_cnt!=0)
426  type=long_double_type();
427  else
428  {
430  error() << "conflicting type modifiers" << eom;
431  throw 0;
432  }
433  }
434  else
435  {
437  error() << "illegal type modifier for float" << eom;
438  throw 0;
439  }
440  }
441  else if(c_bool_cnt)
442  {
446  char_cnt || long_cnt)
447  {
449  error() << "illegal type modifier for C boolean type" << eom;
450  throw 0;
451  }
452 
453  type=c_bool_type();
454  }
455  else if(proper_bool_cnt)
456  {
460  char_cnt || long_cnt)
461  {
463  error() << "illegal type modifier for proper boolean type" << eom;
464  throw 0;
465  }
466 
467  type.id(ID_bool);
468  }
469  else if(complex_cnt && !char_cnt && !signed_cnt && !unsigned_cnt &&
471  {
472  // the "default" for complex is double
473  type=double_type();
474  }
475  else if(char_cnt)
476  {
477  if(int_cnt || short_cnt || long_cnt ||
480  {
482  error() << "illegal type modifier for char type" << eom;
483  throw 0;
484  }
485 
486  if(signed_cnt && unsigned_cnt)
487  {
489  error() << "conflicting type modifiers" << eom;
490  throw 0;
491  }
492  else if(unsigned_cnt)
493  type=unsigned_char_type();
494  else if(signed_cnt)
495  type=signed_char_type();
496  else
497  type=char_type();
498  }
499  else
500  {
501  // it is integer -- signed or unsigned?
502 
503  bool is_signed=true; // default
504 
505  if(signed_cnt && unsigned_cnt)
506  {
508  error() << "conflicting type modifiers" << eom;
509  throw 0;
510  }
511  else if(unsigned_cnt)
512  is_signed=false;
513  else if(signed_cnt)
514  is_signed=true;
515 
517  {
519  {
521  error() << "conflicting type modifiers" << eom;
522  throw 0;
523  }
524 
525  if(int8_cnt)
526  if(is_signed)
527  type=signed_char_type();
528  else
529  type=unsigned_char_type();
530  else if(int16_cnt)
531  if(is_signed)
532  type=signed_short_int_type();
533  else
535  else if(int32_cnt)
536  if(is_signed)
537  type=signed_int_type();
538  else
539  type=unsigned_int_type();
540  else if(int64_cnt) // Visual Studio: equivalent to long long int
541  if(is_signed)
543  else
545  else
546  UNREACHABLE;
547  }
548  else if(gcc_int128_cnt)
549  {
550  if(is_signed)
551  type=gcc_signed_int128_type();
552  else
554  }
555  else if(bv_cnt)
556  {
557  // explicitly-given expression for width
558  type.id(is_signed?ID_custom_signedbv:ID_custom_unsignedbv);
559  type.set(ID_size, bv_width);
560  }
561  else if(floatbv_cnt)
562  {
563  type.id(ID_custom_floatbv);
564  type.set(ID_size, bv_width);
565  type.set(ID_f, fraction_width);
566  }
567  else if(fixedbv_cnt)
568  {
569  type.id(ID_custom_fixedbv);
570  type.set(ID_size, bv_width);
571  type.set(ID_f, fraction_width);
572  }
573  else if(short_cnt)
574  {
575  if(long_cnt || char_cnt)
576  {
578  error() << "conflicting type modifiers" << eom;
579  throw 0;
580  }
581 
582  if(is_signed)
583  type=signed_short_int_type();
584  else
586  }
587  else if(long_cnt==0)
588  {
589  if(is_signed)
590  type=signed_int_type();
591  else
592  type=unsigned_int_type();
593  }
594  else if(long_cnt==1)
595  {
596  if(is_signed)
597  type=signed_long_int_type();
598  else
599  type=unsigned_long_int_type();
600  }
601  else if(long_cnt==2)
602  {
603  if(is_signed)
605  else
607  }
608  else
609  {
611  error() << "illegal type modifier for integer type" << eom;
612  throw 0;
613  }
614  }
615 
617  set_attributes(type);
618 }
619 
622 {
623  if(vector_size.is_not_nil())
624  {
625  type_with_subtypet new_type(ID_frontend_vector, type);
626  new_type.set(ID_size, vector_size);
628  type=new_type;
629  }
630 
631  if(complex_cnt)
632  {
633  // These take more or less arbitrary subtypes.
634  complex_typet new_type(type);
636  type.swap(new_type);
637  }
638 }
639 
642 {
644  {
645  typet new_type=gcc_attribute_mode;
646  new_type.subtype()=type;
647  type.swap(new_type);
648  }
649 
650  c_qualifiers.write(type);
651 
652  if(packed)
653  type.set(ID_C_packed, true);
654 
655  if(aligned)
656  type.set(ID_C_alignment, alignment);
657 }
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
ansi_c_convert_typet::ensures
exprt ensures
Definition: ansi_c_convert_type.h:49
to_unary_expr
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:328
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:463
ansi_c_convert_typet::clear
virtual void clear()
Definition: ansi_c_convert_type.h:70
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:641
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:28
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:501
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:270
ansi_c_convert_typet::source_location
source_locationt source_location
Definition: ansi_c_convert_type.h:60
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
irept::add
irept & add(const irep_namet &name)
Definition: irep.cpp:122
ansi_c_convert_typet::c_qualifiers
c_qualifierst c_qualifiers
Definition: ansi_c_convert_type.h:55
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:112
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
to_type_with_subtypes
const type_with_subtypest & to_type_with_subtypes(const typet &type)
Definition: type.h:198
string_constant.h
exprt
Base class for all expressions.
Definition: expr.h:54
complex_typet
Complex numbers made of pair of given subtype.
Definition: std_types.h:1009
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:391
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:738
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
ansi_c_convert_typet::requires
exprt requires
Definition: ansi_c_convert_type.h:49
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:453
irept::is_nil
bool is_nil() const
Definition: irep.h:387
irept::id
const irep_idt & id() const
Definition: irep.h:407
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:293
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:62
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:243
ansi_c_convert_typet::c_storage_spec
c_storage_spect c_storage_spec
Definition: ansi_c_convert_type.h:52
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:621
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:431
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:994
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:639
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:24
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:383
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:117
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: pointer_expr.h:24
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:238
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:31
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
ansi_c_convert_typet::assigns
exprt assigns
Definition: ansi_c_convert_type.h:49