cprover
c_typecast.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_typecast.h"
10 
11 #include <algorithm>
12 
13 #include <cassert>
14 
15 #include <util/arith_tools.h>
16 #include <util/c_types.h>
17 #include <util/config.h>
18 #include <util/expr_util.h>
20 #include <util/simplify_expr.h>
21 #include <util/std_expr.h>
22 #include <util/symbol.h>
23 
24 #include "c_qualifiers.h"
25 
27  exprt &expr,
28  const typet &dest_type,
29  const namespacet &ns)
30 {
31  c_typecastt c_typecast(ns);
32  c_typecast.implicit_typecast(expr, dest_type);
33  return !c_typecast.errors.empty();
34 }
35 
37  const typet &src_type,
38  const typet &dest_type,
39  const namespacet &ns)
40 {
41  c_typecastt c_typecast(ns);
42  exprt tmp;
43  tmp.type()=src_type;
44  c_typecast.implicit_typecast(tmp, dest_type);
45  return !c_typecast.errors.empty();
46 }
47 
50  exprt &expr1, exprt &expr2,
51  const namespacet &ns)
52 {
53  c_typecastt c_typecast(ns);
54  c_typecast.implicit_typecast_arithmetic(expr1, expr2);
55  return !c_typecast.errors.empty();
56 }
57 
58 bool has_a_void_pointer(const typet &type)
59 {
60  if(type.id()==ID_pointer)
61  {
62  if(type.subtype().id()==ID_empty)
63  return true;
64 
65  return has_a_void_pointer(type.subtype());
66  }
67  else
68  return false;
69 }
70 
72  const typet &src_type,
73  const typet &dest_type)
74 {
75  // check qualifiers
76 
77  if(src_type.id()==ID_pointer && dest_type.id()==ID_pointer &&
78  src_type.subtype().get_bool(ID_C_constant) &&
79  !dest_type.subtype().get_bool(ID_C_constant))
80  return true;
81 
82  if(src_type==dest_type)
83  return false;
84 
85  const irep_idt &src_type_id=src_type.id();
86 
87  if(src_type_id==ID_c_bit_field)
88  return check_c_implicit_typecast(src_type.subtype(), dest_type);
89 
90  if(dest_type.id()==ID_c_bit_field)
91  return check_c_implicit_typecast(src_type, dest_type.subtype());
92 
93  if(src_type_id==ID_natural)
94  {
95  if(dest_type.id()==ID_bool ||
96  dest_type.id()==ID_c_bool ||
97  dest_type.id()==ID_integer ||
98  dest_type.id()==ID_real ||
99  dest_type.id()==ID_complex ||
100  dest_type.id()==ID_unsignedbv ||
101  dest_type.id()==ID_signedbv ||
102  dest_type.id()==ID_floatbv ||
103  dest_type.id()==ID_complex)
104  return false;
105  }
106  else if(src_type_id==ID_integer)
107  {
108  if(dest_type.id()==ID_bool ||
109  dest_type.id()==ID_c_bool ||
110  dest_type.id()==ID_real ||
111  dest_type.id()==ID_complex ||
112  dest_type.id()==ID_unsignedbv ||
113  dest_type.id()==ID_signedbv ||
114  dest_type.id()==ID_floatbv ||
115  dest_type.id()==ID_fixedbv ||
116  dest_type.id()==ID_pointer ||
117  dest_type.id()==ID_complex)
118  return false;
119  }
120  else if(src_type_id==ID_real)
121  {
122  if(dest_type.id()==ID_bool ||
123  dest_type.id()==ID_c_bool ||
124  dest_type.id()==ID_complex ||
125  dest_type.id()==ID_floatbv ||
126  dest_type.id()==ID_fixedbv ||
127  dest_type.id()==ID_complex)
128  return false;
129  }
130  else if(src_type_id==ID_rational)
131  {
132  if(dest_type.id()==ID_bool ||
133  dest_type.id()==ID_c_bool ||
134  dest_type.id()==ID_complex ||
135  dest_type.id()==ID_floatbv ||
136  dest_type.id()==ID_fixedbv ||
137  dest_type.id()==ID_complex)
138  return false;
139  }
140  else if(src_type_id==ID_bool)
141  {
142  if(dest_type.id()==ID_c_bool ||
143  dest_type.id()==ID_integer ||
144  dest_type.id()==ID_real ||
145  dest_type.id()==ID_unsignedbv ||
146  dest_type.id()==ID_signedbv ||
147  dest_type.id()==ID_pointer ||
148  dest_type.id()==ID_floatbv ||
149  dest_type.id()==ID_fixedbv ||
150  dest_type.id()==ID_c_enum ||
151  dest_type.id()==ID_c_enum_tag ||
152  dest_type.id()==ID_complex)
153  return false;
154  }
155  else if(src_type_id==ID_unsignedbv ||
156  src_type_id==ID_signedbv ||
157  src_type_id==ID_c_enum ||
158  src_type_id==ID_c_enum_tag ||
159  src_type_id==ID_c_bool)
160  {
161  if(dest_type.id()==ID_unsignedbv ||
162  dest_type.id()==ID_bool ||
163  dest_type.id()==ID_c_bool ||
164  dest_type.id()==ID_integer ||
165  dest_type.id()==ID_real ||
166  dest_type.id()==ID_rational ||
167  dest_type.id()==ID_signedbv ||
168  dest_type.id()==ID_floatbv ||
169  dest_type.id()==ID_fixedbv ||
170  dest_type.id()==ID_pointer ||
171  dest_type.id()==ID_c_enum ||
172  dest_type.id()==ID_c_enum_tag ||
173  dest_type.id()==ID_complex)
174  return false;
175  }
176  else if(src_type_id==ID_floatbv ||
177  src_type_id==ID_fixedbv)
178  {
179  if(dest_type.id()==ID_bool ||
180  dest_type.id()==ID_c_bool ||
181  dest_type.id()==ID_integer ||
182  dest_type.id()==ID_real ||
183  dest_type.id()==ID_rational ||
184  dest_type.id()==ID_signedbv ||
185  dest_type.id()==ID_unsignedbv ||
186  dest_type.id()==ID_floatbv ||
187  dest_type.id()==ID_fixedbv ||
188  dest_type.id()==ID_complex)
189  return false;
190  }
191  else if(src_type_id==ID_complex)
192  {
193  if(dest_type.id()==ID_complex)
194  return check_c_implicit_typecast(src_type.subtype(), dest_type.subtype());
195  else
196  {
197  // 6.3.1.7, par 2:
198 
199  // When a value of complex type is converted to a real type, the
200  // imaginary part of the complex value is discarded and the value of the
201  // real part is converted according to the conversion rules for the
202  // corresponding real type.
203 
204  return check_c_implicit_typecast(src_type.subtype(), dest_type);
205  }
206  }
207  else if(src_type_id==ID_array ||
208  src_type_id==ID_pointer)
209  {
210  if(dest_type.id()==ID_pointer)
211  {
212  const irept &dest_subtype=dest_type.subtype();
213  const irept &src_subtype =src_type.subtype();
214 
215  if(src_subtype == dest_subtype)
216  {
217  return false;
218  }
219  else if(
220  has_a_void_pointer(src_type) || // from void to anything
221  has_a_void_pointer(dest_type)) // to void from anything
222  {
223  return false;
224  }
225  }
226 
227  if(dest_type.id()==ID_array &&
228  src_type.subtype()==dest_type.subtype())
229  return false;
230 
231  if(dest_type.id()==ID_bool ||
232  dest_type.id()==ID_c_bool ||
233  dest_type.id()==ID_unsignedbv ||
234  dest_type.id()==ID_signedbv)
235  return false;
236  }
237  else if(src_type_id==ID_vector)
238  {
239  if(dest_type.id()==ID_vector)
240  return false;
241  }
242  else if(src_type_id==ID_complex)
243  {
244  if(dest_type.id()==ID_complex)
245  {
246  // We convert between complex types if we convert between
247  // their component types.
248  if(!check_c_implicit_typecast(src_type.subtype(), dest_type.subtype()))
249  return false;
250  }
251  }
252 
253  return true;
254 }
255 
257 {
258  if(
259  src_type.id() != ID_struct_tag &&
260  src_type.id() != ID_union_tag)
261  {
262  return src_type;
263  }
264 
265  typet result_type=src_type;
266 
267  // collect qualifiers
268  c_qualifierst qualifiers(src_type);
269 
270  while(result_type.id() == ID_struct_tag || result_type.id() == ID_union_tag)
271  {
272  const typet &followed_type = ns.follow(result_type);
273  result_type = followed_type;
274  qualifiers += c_qualifierst(followed_type);
275  }
276 
277  qualifiers.write(result_type);
278 
279  return result_type;
280 }
281 
283  const typet &type) const
284 {
285  if(type.id()==ID_signedbv)
286  {
287  const std::size_t width = to_bitvector_type(type).get_width();
288 
289  if(width<=config.ansi_c.char_width)
290  return CHAR;
291  else if(width<=config.ansi_c.short_int_width)
292  return SHORT;
293  else if(width<=config.ansi_c.int_width)
294  return INT;
295  else if(width<=config.ansi_c.long_int_width)
296  return LONG;
297  else if(width<=config.ansi_c.long_long_int_width)
298  return LONGLONG;
299  else
300  return LARGE_SIGNED_INT;
301  }
302  else if(type.id()==ID_unsignedbv)
303  {
304  const std::size_t width = to_bitvector_type(type).get_width();
305 
306  if(width<=config.ansi_c.char_width)
307  return UCHAR;
308  else if(width<=config.ansi_c.short_int_width)
309  return USHORT;
310  else if(width<=config.ansi_c.int_width)
311  return UINT;
312  else if(width<=config.ansi_c.long_int_width)
313  return ULONG;
314  else if(width<=config.ansi_c.long_long_int_width)
315  return ULONGLONG;
316  else
317  return LARGE_UNSIGNED_INT;
318  }
319  else if(type.id()==ID_bool)
320  return BOOL;
321  else if(type.id()==ID_c_bool)
322  return BOOL;
323  else if(type.id()==ID_floatbv)
324  {
325  const std::size_t width = to_bitvector_type(type).get_width();
326 
327  if(width<=config.ansi_c.single_width)
328  return SINGLE;
329  else if(width<=config.ansi_c.double_width)
330  return DOUBLE;
331  else if(width<=config.ansi_c.long_double_width)
332  return LONGDOUBLE;
333  else if(width<=128)
334  return FLOAT128;
335  }
336  else if(type.id()==ID_fixedbv)
337  {
338  return FIXEDBV;
339  }
340  else if(type.id()==ID_pointer)
341  {
342  if(type.subtype().id()==ID_empty)
343  return VOIDPTR;
344  else
345  return PTR;
346  }
347  else if(type.id()==ID_array)
348  {
349  return PTR;
350  }
351  else if(type.id() == ID_c_enum || type.id() == ID_c_enum_tag)
352  {
353  return INT;
354  }
355  else if(type.id()==ID_rational)
356  return RATIONAL;
357  else if(type.id()==ID_real)
358  return REAL;
359  else if(type.id()==ID_complex)
360  return COMPLEX;
361  else if(type.id()==ID_c_bit_field)
362  {
363  const auto &bit_field_type = to_c_bit_field_type(type);
364 
365  // We take the underlying type, and then apply the number
366  // of bits given
367  typet underlying_type;
368 
369  if(bit_field_type.subtype().id() == ID_c_enum_tag)
370  {
371  const auto &followed =
372  ns.follow_tag(to_c_enum_tag_type(bit_field_type.subtype()));
373  if(followed.is_incomplete())
374  return INT;
375  else
376  underlying_type = followed.subtype();
377  }
378  else
379  underlying_type = bit_field_type.subtype();
380 
381  const bitvector_typet new_type(
382  underlying_type.id(), bit_field_type.get_width());
383 
384  return get_c_type(new_type);
385  }
386 
387  return OTHER;
388 }
389 
391  exprt &expr,
392  c_typet c_type)
393 {
394  typet new_type;
395 
396  switch(c_type)
397  {
398  case PTR:
399  if(expr.type().id() == ID_array)
400  {
401  new_type = pointer_type(expr.type().subtype());
402  break;
403  }
404  return;
405 
406  case BOOL: UNREACHABLE; // should always be promoted to int
407  case CHAR: UNREACHABLE; // should always be promoted to int
408  case UCHAR: UNREACHABLE; // should always be promoted to int
409  case SHORT: UNREACHABLE; // should always be promoted to int
410  case USHORT: UNREACHABLE; // should always be promoted to int
411  case INT: new_type=signed_int_type(); break;
412  case UINT: new_type=unsigned_int_type(); break;
413  case LONG: new_type=signed_long_int_type(); break;
414  case ULONG: new_type=unsigned_long_int_type(); break;
415  case LONGLONG: new_type=signed_long_long_int_type(); break;
416  case ULONGLONG: new_type=unsigned_long_long_int_type(); break;
417  case SINGLE: new_type=float_type(); break;
418  case DOUBLE: new_type=double_type(); break;
419  case LONGDOUBLE: new_type=long_double_type(); break;
420  // NOLINTNEXTLINE(whitespace/line_length)
421  case FLOAT128: new_type=ieee_float_spect::quadruple_precision().to_type(); break;
422  case RATIONAL: new_type=rational_typet(); break;
423  case REAL: new_type=real_typet(); break;
424  case INTEGER: new_type=integer_typet(); break;
425  case COMPLEX:
426  case OTHER:
427  case VOIDPTR:
428  case FIXEDBV:
429  case LARGE_UNSIGNED_INT:
430  case LARGE_SIGNED_INT:
431  return; // do nothing
432  }
433 
434  if(new_type != expr.type())
435  do_typecast(expr, new_type);
436 }
437 
439  const typet &type) const
440 {
441  c_typet c_type=get_c_type(type);
442 
443  // 6.3.1.1, par 2
444 
445  // "If an int can represent all values of the original type, the
446  // value is converted to an int; otherwise, it is converted to
447  // an unsigned int."
448 
449  c_typet max_type=std::max(c_type, INT); // minimum promotion
450 
451  // The second case can arise if we promote any unsigned type
452  // that is as large as unsigned int. In this case the promotion configuration
453  // via the enum is actually wrong, and we need to fix this up.
454  if(
456  c_type == USHORT)
457  max_type=UINT;
458  else if(
460  max_type=UINT;
461 
462  if(max_type==UINT &&
463  type.id()==ID_c_bit_field &&
464  to_c_bit_field_type(type).get_width()<config.ansi_c.int_width)
465  max_type=INT;
466 
467  return max_type;
468 }
469 
471 {
472  c_typet c_type=minimum_promotion(expr.type());
473  implicit_typecast_arithmetic(expr, c_type);
474 }
475 
477  exprt &expr,
478  const typet &type)
479 {
480  typet src_type=follow_with_qualifiers(expr.type()),
481  dest_type=follow_with_qualifiers(type);
482 
483  typet type_qual=type;
484  c_qualifierst qualifiers(dest_type);
485  qualifiers.write(type_qual);
486 
487  implicit_typecast_followed(expr, src_type, type_qual, dest_type);
488 }
489 
491  exprt &expr,
492  const typet &src_type,
493  const typet &orig_dest_type,
494  const typet &dest_type)
495 {
496  // do transparent union
497  if(dest_type.id()==ID_union &&
498  dest_type.get_bool(ID_C_transparent_union) &&
499  src_type.id()!=ID_union)
500  {
501  // The argument corresponding to a transparent union type can be of any
502  // type in the union; no explicit cast is required.
503 
504  // GCC docs say:
505  // If the union member type is a pointer, qualifiers like const on the
506  // referenced type must be respected, just as with normal pointer
507  // conversions.
508  // But it is accepted, and Clang doesn't even emit a warning (GCC 4.7 does)
509  typet src_type_no_const=src_type;
510  if(src_type.id()==ID_pointer &&
511  src_type.subtype().get_bool(ID_C_constant))
512  src_type_no_const.subtype().remove(ID_C_constant);
513 
514  // Check union members.
515  for(const auto &comp : to_union_type(dest_type).components())
516  {
517  if(!check_c_implicit_typecast(src_type_no_const, comp.type()))
518  {
519  // build union constructor
520  union_exprt union_expr(comp.get_name(), expr, orig_dest_type);
521  if(!src_type.full_eq(src_type_no_const))
522  do_typecast(union_expr.op(), src_type_no_const);
523  expr=union_expr;
524  return; // ok
525  }
526  }
527  }
528 
529  if(dest_type.id()==ID_pointer)
530  {
531  // special case: 0 == NULL
532 
533  if(simplify_expr(expr, ns).is_zero() && (
534  src_type.id()==ID_unsignedbv ||
535  src_type.id()==ID_signedbv ||
536  src_type.id()==ID_natural ||
537  src_type.id()==ID_integer))
538  {
539  expr=exprt(ID_constant, orig_dest_type);
540  expr.set(ID_value, ID_NULL);
541  return; // ok
542  }
543 
544  if(src_type.id()==ID_pointer ||
545  src_type.id()==ID_array)
546  {
547  // we are quite generous about pointers
548 
549  const typet &src_sub = src_type.subtype();
550  const typet &dest_sub = dest_type.subtype();
551 
552  if(has_a_void_pointer(src_type) || has_a_void_pointer(dest_type))
553  {
554  // from/to void is always good
555  }
556  else if(src_sub.id()==ID_code &&
557  dest_sub.id()==ID_code)
558  {
559  // very generous:
560  // between any two function pointers it's ok
561  }
562  else if(src_sub == dest_sub)
563  {
564  // ok
565  }
566  else if((is_number(src_sub) ||
567  src_sub.id()==ID_c_enum ||
568  src_sub.id()==ID_c_enum_tag) &&
569  (is_number(dest_sub) ||
570  dest_sub.id()==ID_c_enum ||
571  src_sub.id()==ID_c_enum_tag))
572  {
573  // Also generous: between any to scalar types it's ok.
574  // We should probably check the size.
575  }
576  else if(
577  src_sub.id() == ID_array && dest_sub.id() == ID_array &&
578  src_sub.subtype() == dest_sub.subtype())
579  {
580  // we ignore the size of the top-level array
581  // in the case of pointers to arrays
582  }
583  else
584  warnings.push_back("incompatible pointer types");
585 
586  // check qualifiers
587 
588  if(src_type.subtype().get_bool(ID_C_volatile) &&
589  !dest_type.subtype().get_bool(ID_C_volatile))
590  warnings.push_back("disregarding volatile");
591 
592  if(src_type==dest_type)
593  {
594  expr.type()=src_type; // because of qualifiers
595  }
596  else
597  do_typecast(expr, orig_dest_type);
598 
599  return; // ok
600  }
601  }
602 
603  if(check_c_implicit_typecast(src_type, dest_type))
604  errors.push_back("implicit conversion not permitted");
605  else if(src_type!=dest_type)
606  do_typecast(expr, orig_dest_type);
607 }
608 
610  exprt &expr1,
611  exprt &expr2)
612 {
613  const typet &type1 = expr1.type();
614  const typet &type2 = expr2.type();
615 
616  c_typet c_type1=minimum_promotion(type1),
617  c_type2=minimum_promotion(type2);
618 
619  c_typet max_type=std::max(c_type1, c_type2);
620 
621  if(max_type==LARGE_SIGNED_INT || max_type==LARGE_UNSIGNED_INT)
622  {
623  // get the biggest width of both
624  std::size_t width1 = to_bitvector_type(type1).get_width();
625  std::size_t width2 = to_bitvector_type(type2).get_width();
626 
627  // produce type
628  typet result_type;
629 
630  if(width1==width2)
631  {
632  if(max_type==LARGE_SIGNED_INT)
633  result_type=signedbv_typet(width1);
634  else
635  result_type=unsignedbv_typet(width1);
636  }
637  else if(width1>width2)
638  result_type=type1;
639  else // width1<width2
640  result_type=type2;
641 
642  do_typecast(expr1, result_type);
643  do_typecast(expr2, result_type);
644 
645  return;
646  }
647  else if(max_type==FIXEDBV)
648  {
649  typet result_type;
650 
651  if(c_type1==FIXEDBV && c_type2==FIXEDBV)
652  {
653  // get bigger of both
654  std::size_t width1=to_fixedbv_type(type1).get_width();
655  std::size_t width2=to_fixedbv_type(type2).get_width();
656  if(width1>=width2)
657  result_type=type1;
658  else
659  result_type=type2;
660  }
661  else if(c_type1==FIXEDBV)
662  result_type=type1;
663  else
664  result_type=type2;
665 
666  do_typecast(expr1, result_type);
667  do_typecast(expr2, result_type);
668 
669  return;
670  }
671  else if(max_type==COMPLEX)
672  {
673  if(c_type1==COMPLEX && c_type2==COMPLEX)
674  {
675  // promote to the one with bigger subtype
676  if(get_c_type(type1.subtype())>get_c_type(type2.subtype()))
677  do_typecast(expr2, type1);
678  else
679  do_typecast(expr1, type2);
680  }
681  else if(c_type1==COMPLEX)
682  {
683  assert(c_type1==COMPLEX && c_type2!=COMPLEX);
684  do_typecast(expr2, type1.subtype());
685  do_typecast(expr2, type1);
686  }
687  else
688  {
689  assert(c_type1!=COMPLEX && c_type2==COMPLEX);
690  do_typecast(expr1, type2.subtype());
691  do_typecast(expr1, type2);
692  }
693 
694  return;
695  }
696  else if(max_type==SINGLE || max_type==DOUBLE ||
697  max_type==LONGDOUBLE || max_type==FLOAT128)
698  {
699  // Special-case optimisation:
700  // If we have two non-standard sized floats, don't do implicit type
701  // promotion if we can possibly avoid it.
702  if(type1==type2)
703  return;
704  }
705 
706  implicit_typecast_arithmetic(expr1, max_type);
707  implicit_typecast_arithmetic(expr2, max_type);
708 
709  // arithmetic typecasts only, otherwise this can't be used from
710  // typecheck_expr_trinary
711  #if 0
712  if(max_type==PTR)
713  {
714  if(c_type1==VOIDPTR)
715  do_typecast(expr1, expr2.type());
716 
717  if(c_type2==VOIDPTR)
718  do_typecast(expr2, expr1.type());
719  }
720  #endif
721 }
722 
723 void c_typecastt::do_typecast(exprt &expr, const typet &dest_type)
724 {
725  // special case: array -> pointer is actually
726  // something like address_of
727 
728  const typet &src_type = expr.type();
729 
730  if(src_type.id()==ID_array)
731  {
732  index_exprt index(expr, from_integer(0, index_type()));
733  expr = typecast_exprt::conditional_cast(address_of_exprt(index), dest_type);
734  return;
735  }
736 
737  if(src_type!=dest_type)
738  {
739  // C booleans are special; we produce the
740  // explicit comparison with zero.
741  // Note that this requires ieee_float_notequal
742  // in case of floating-point numbers.
743 
744  if(dest_type.get(ID_C_c_type)==ID_bool)
745  {
746  expr = typecast_exprt(is_not_zero(expr, ns), dest_type);
747  }
748  else if(dest_type.id()==ID_bool)
749  {
750  expr=is_not_zero(expr, ns);
751  }
752  else
753  {
754  expr = typecast_exprt(expr, dest_type);
755  }
756  }
757 }
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
c_typecastt::ns
const namespacet & ns
Definition: c_typecast.h:67
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
to_c_enum_tag_type
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Definition: std_types.h:721
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2021
typet::subtype
const typet & subtype() const
Definition: type.h:47
c_typecastt::LONGLONG
@ LONGLONG
Definition: c_typecast.h:76
arith_tools.h
is_number
bool is_number(const typet &type)
Returns true if the type is a rational, real, integer, natural, complex, unsignedbv,...
Definition: mathematical_types.cpp:17
signed_long_long_int_type
signedbv_typet signed_long_long_int_type()
Definition: c_types.cpp:87
c_typecastt
Definition: c_typecast.h:42
rational_typet
Unbounded, signed rational numbers.
Definition: mathematical_types.h:40
irept::full_eq
bool full_eq(const irept &other) const
Definition: irep.cpp:202
typet
The type of an expression, extends irept.
Definition: type.h:29
c_typecastt::COMPLEX
@ COMPLEX
Definition: c_typecast.h:82
long_double_type
floatbv_typet long_double_type()
Definition: c_types.cpp:201
c_typecastt::SINGLE
@ SINGLE
Definition: c_typecast.h:80
c_typecastt::INT
@ INT
Definition: c_typecast.h:74
union_exprt
Union constructor from single element.
Definition: std_expr.h:1567
integer_typet
Unbounded, signed integers (mathematical integers, not bitvectors)
Definition: mathematical_types.h:22
c_typecastt::BOOL
@ BOOL
Definition: c_typecast.h:71
exprt
Base class for all expressions.
Definition: expr.h:53
ieee_float_spect::quadruple_precision
static ieee_float_spect quadruple_precision()
Definition: ieee_float.h:86
namespace_baset::follow_tag
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:65
c_implicit_typecast_arithmetic
bool c_implicit_typecast_arithmetic(exprt &expr1, exprt &expr2, const namespacet &ns)
perform arithmetic prompotions and conversions
Definition: c_typecast.cpp:49
c_qualifiers.h
c_typecastt::minimum_promotion
c_typet minimum_promotion(const typet &type) const
Definition: c_typecast.cpp:438
configt::ansi_c
struct configt::ansi_ct ansi_c
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
c_typecastt::UCHAR
@ UCHAR
Definition: c_typecast.h:72
unsignedbv_typet
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1216
unsigned_long_long_int_type
unsignedbv_typet unsigned_long_long_int_type()
Definition: c_types.cpp:101
c_typecastt::LONG
@ LONG
Definition: c_typecast.h:75
configt::ansi_ct::char_width
std::size_t char_width
Definition: config.h:34
mathematical_types.h
Mathematical types.
unsigned_long_int_type
unsignedbv_typet unsigned_long_int_type()
Definition: c_types.cpp:94
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
c_typecastt::get_c_type
c_typet get_c_type(const typet &type) const
Definition: c_typecast.cpp:282
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
c_typecastt::warnings
std::list< std::string > warnings
Definition: c_typecast.h:64
real_typet
Unbounded, signed real numbers.
Definition: mathematical_types.h:49
to_fixedbv_type
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
Definition: std_types.h:1362
signed_int_type
signedbv_typet signed_int_type()
Definition: c_types.cpp:30
check_c_implicit_typecast
bool check_c_implicit_typecast(const typet &src_type, const typet &dest_type, const namespacet &ns)
Definition: c_typecast.cpp:36
configt::ansi_ct::double_width
std::size_t double_width
Definition: config.h:39
c_typecastt::INTEGER
@ INTEGER
Definition: c_typecast.h:78
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:1265
to_c_bit_field_type
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
Definition: std_types.h:1471
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
configt::ansi_ct::long_long_int_width
std::size_t long_long_int_width
Definition: config.h:36
simplify_expr
exprt simplify_expr(exprt src, const namespacet &ns)
Definition: simplify_expr.cpp:2698
c_typecastt::LARGE_SIGNED_INT
@ LARGE_SIGNED_INT
Definition: c_typecast.h:77
c_typecastt::REAL
@ REAL
Definition: c_typecast.h:81
c_qualifierst
Definition: c_qualifiers.h:61
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
symbol.h
Symbol table entry.
irept::id
const irep_idt & id() const
Definition: irep.h:418
irept::remove
void remove(const irep_namet &name)
Definition: irep.cpp:93
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:281
c_implicit_typecast
bool c_implicit_typecast(exprt &expr, const typet &dest_type, const namespacet &ns)
Definition: c_typecast.cpp:26
c_typecastt::USHORT
@ USHORT
Definition: c_typecast.h:73
c_typecastt::PTR
@ PTR
Definition: c_typecast.h:83
c_typecastt::implicit_typecast_followed
virtual void implicit_typecast_followed(exprt &expr, const typet &src_type, const typet &orig_dest_type, const typet &dest_type)
Definition: c_typecast.cpp:490
double_type
floatbv_typet double_type()
Definition: c_types.cpp:193
config
configt config
Definition: config.cpp:24
c_typecastt::UINT
@ UINT
Definition: c_typecast.h:74
simplify_expr.h
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:1041
c_typecastt::LONGDOUBLE
@ LONGDOUBLE
Definition: c_typecast.h:80
expr_util.h
Deprecated expression utility functions.
c_typecastt::VOIDPTR
@ VOIDPTR
Definition: c_typecast.h:83
c_typecastt::FLOAT128
@ FLOAT128
Definition: c_typecast.h:80
has_a_void_pointer
bool has_a_void_pointer(const typet &type)
Definition: c_typecast.cpp:58
c_typecastt::implicit_typecast_arithmetic
virtual void implicit_typecast_arithmetic(exprt &expr)
Definition: c_typecast.cpp:470
bitvector_typet
Base class of fixed-width bit-vector types.
Definition: std_types.h:1030
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
c_typecast.h
is_not_zero
exprt is_not_zero(const exprt &src, const namespacet &ns)
converts a scalar/float expression to C/C++ Booleans
Definition: expr_util.cpp:98
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:442
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
c_typecastt::errors
std::list< std::string > errors
Definition: c_typecast.h:63
configt::ansi_ct::long_double_width
std::size_t long_double_width
Definition: config.h:40
c_typecastt::ULONGLONG
@ ULONGLONG
Definition: c_typecast.h:76
c_typecastt::LARGE_UNSIGNED_INT
@ LARGE_UNSIGNED_INT
Definition: c_typecast.h:77
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
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:394
c_typecastt::c_typet
c_typet
Definition: c_typecast.h:71
c_typecastt::SHORT
@ SHORT
Definition: c_typecast.h:73
c_typecastt::CHAR
@ CHAR
Definition: c_typecast.h:72
to_union_type
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: std_types.h:422
index_exprt
Array index operator.
Definition: std_expr.h:1293
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:2786
configt::ansi_ct::single_width
std::size_t single_width
Definition: config.h:38
c_typecastt::OTHER
@ OTHER
Definition: c_typecast.h:83
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2013
c_typecastt::ULONG
@ ULONG
Definition: c_typecast.h:75
c_typecastt::implicit_typecast
virtual void implicit_typecast(exprt &expr, const typet &type)
Definition: c_typecast.cpp:476
c_typecastt::follow_with_qualifiers
typet follow_with_qualifiers(const typet &src)
Definition: c_typecast.cpp:256
c_typecastt::do_typecast
void do_typecast(exprt &dest, const typet &type)
Definition: c_typecast.cpp:723
c_typecastt::DOUBLE
@ DOUBLE
Definition: c_typecast.h:80
std_expr.h
API to expression classes.
c_typecastt::RATIONAL
@ RATIONAL
Definition: c_typecast.h:81
configt::ansi_ct::int_width
std::size_t int_width
Definition: config.h:31
c_types.h
c_typecastt::FIXEDBV
@ FIXEDBV
Definition: c_typecast.h:79
configt::ansi_ct::long_int_width
std::size_t long_int_width
Definition: config.h:32
to_bitvector_type
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: std_types.h:1089