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