CBMC
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 <util/arith_tools.h>
12#include <util/c_types.h>
13#include <util/config.h>
14#include <util/expr_util.h>
16#include <util/namespace.h>
17#include <util/pointer_expr.h>
18#include <util/rational.h>
19#include <util/rational_tools.h>
20#include <util/simplify_expr.h>
21#include <util/std_expr.h>
22
23#include "c_qualifiers.h"
24
25#include <algorithm>
26
28 exprt &expr,
29 const typet &dest_type,
30 const namespacet &ns)
31{
33 c_typecast.implicit_typecast(expr, dest_type);
34 return !c_typecast.errors.empty();
35}
36
38 const typet &src_type,
39 const typet &dest_type,
40 const namespacet &ns)
41{
43 exprt tmp;
44 tmp.type()=src_type;
45 c_typecast.implicit_typecast(tmp, dest_type);
46 return !c_typecast.errors.empty();
47}
48
52 const namespacet &ns)
53{
55 c_typecast.implicit_typecast_arithmetic(expr1, expr2);
56 return !c_typecast.errors.empty();
57}
58
59bool has_a_void_pointer(const typet &type)
60{
61 if(type.id()==ID_pointer)
62 {
63 const auto &pointer_type = to_pointer_type(type);
64
65 if(pointer_type.base_type().id() == ID_empty)
66 return true;
67
69 }
70 else
71 return false;
72}
73
75 const typet &src_type,
76 const typet &dest_type)
77{
78 // check qualifiers
79
80 if(
81 src_type.id() == ID_pointer && dest_type.id() == ID_pointer &&
82 to_pointer_type(src_type).base_type().get_bool(ID_C_constant) &&
83 !to_pointer_type(dest_type).base_type().get_bool(ID_C_constant))
84 {
85 return true;
86 }
87
89 return false;
90
91 const irep_idt &src_type_id=src_type.id();
92
94 {
96 to_c_bit_field_type(src_type).underlying_type(), dest_type);
97 }
98
100 {
102 src_type, to_c_bit_field_type(dest_type).underlying_type());
103 }
104
106 {
107 if(
108 dest_type.id() == ID_bool || dest_type.id() == ID_c_bool ||
109 dest_type.id() == ID_integer || dest_type.id() == ID_rational ||
110 dest_type.id() == ID_real || dest_type.id() == ID_complex ||
111 dest_type.id() == ID_unsignedbv || dest_type.id() == ID_signedbv ||
112 dest_type.id() == ID_floatbv || dest_type.id() == ID_complex)
113 {
114 return false;
115 }
116 }
117 else if(src_type_id==ID_integer)
118 {
119 if(
120 dest_type.id() == ID_bool || dest_type.id() == ID_c_bool ||
121 dest_type.id() == ID_natural || dest_type.id() == ID_rational ||
122 dest_type.id() == ID_real || dest_type.id() == ID_complex ||
123 dest_type.id() == ID_unsignedbv || dest_type.id() == ID_signedbv ||
124 dest_type.id() == ID_floatbv || dest_type.id() == ID_fixedbv ||
125 dest_type.id() == ID_pointer || dest_type.id() == ID_complex)
126 {
127 return false;
128 }
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(
143 dest_type.id() == ID_bool || dest_type.id() == ID_c_bool ||
144 dest_type.id() == ID_real || dest_type.id() == ID_complex ||
145 dest_type.id() == ID_floatbv || dest_type.id() == ID_fixedbv ||
146 dest_type.id() == ID_complex)
147 {
148 return false;
149 }
150 }
151 else if(src_type_id==ID_bool)
152 {
153 if(
154 dest_type.id() == ID_c_bool || dest_type.id() == ID_integer ||
155 dest_type.id() == ID_natural || dest_type.id() == ID_rational ||
156 dest_type.id() == ID_real || dest_type.id() == ID_unsignedbv ||
157 dest_type.id() == ID_signedbv || dest_type.id() == ID_pointer ||
158 dest_type.id() == ID_floatbv || dest_type.id() == ID_fixedbv ||
159 dest_type.id() == ID_c_enum || dest_type.id() == ID_c_enum_tag ||
160 dest_type.id() == ID_complex)
161 {
162 return false;
163 }
164 }
165 else if(src_type_id==ID_unsignedbv ||
170 {
171 if(
172 dest_type.id() == ID_unsignedbv || dest_type.id() == ID_bool ||
173 dest_type.id() == ID_c_bool || dest_type.id() == ID_integer ||
174 dest_type.id() == ID_natural || dest_type.id() == ID_rational ||
175 dest_type.id() == ID_real || dest_type.id() == ID_signedbv ||
176 dest_type.id() == ID_floatbv || dest_type.id() == ID_fixedbv ||
177 dest_type.id() == ID_pointer || dest_type.id() == ID_c_enum ||
178 dest_type.id() == ID_c_enum_tag || dest_type.id() == ID_complex)
179 {
180 return false;
181 }
182 }
183 else if(src_type_id==ID_floatbv ||
185 {
186 if(dest_type.id()==ID_bool ||
187 dest_type.id()==ID_c_bool ||
188 dest_type.id()==ID_integer ||
189 dest_type.id()==ID_real ||
190 dest_type.id()==ID_rational ||
191 dest_type.id()==ID_signedbv ||
192 dest_type.id()==ID_unsignedbv ||
193 dest_type.id()==ID_floatbv ||
194 dest_type.id()==ID_fixedbv ||
195 dest_type.id()==ID_complex)
196 return false;
197 }
198 else if(src_type_id==ID_complex)
199 {
200 if(dest_type.id()==ID_complex)
201 {
203 to_complex_type(src_type).subtype(),
204 to_complex_type(dest_type).subtype());
205 }
206 else
207 {
208 // 6.3.1.7, par 2:
209
210 // When a value of complex type is converted to a real type, the
211 // imaginary part of the complex value is discarded and the value of the
212 // real part is converted according to the conversion rules for the
213 // corresponding real type.
214
217 }
218 }
219 else if(src_type_id==ID_array ||
221 {
222 if(dest_type.id()==ID_pointer)
223 {
224 const irept &dest_subtype = to_pointer_type(dest_type).base_type();
226
228 {
229 return false;
230 }
231 else if(
232 has_a_void_pointer(src_type) || // from void to anything
233 has_a_void_pointer(dest_type)) // to void from anything
234 {
235 return false;
236 }
237 }
238
239 if(
240 dest_type.id() == ID_array && to_type_with_subtype(src_type).subtype() ==
241 to_array_type(dest_type).element_type())
242 {
243 return false;
244 }
245
246 if(dest_type.id()==ID_bool ||
247 dest_type.id()==ID_c_bool ||
248 dest_type.id()==ID_unsignedbv ||
250 return false;
251 }
252 else if(src_type_id==ID_vector)
253 {
254 if(dest_type.id()==ID_vector)
255 return false;
256 }
257 else if(src_type_id==ID_complex)
258 {
259 if(dest_type.id()==ID_complex)
260 {
261 // We convert between complex types if we convert between
262 // their component types.
264 to_complex_type(src_type).subtype(),
265 to_complex_type(dest_type).subtype()))
266 {
267 return false;
268 }
269 }
270 }
271
272 return true;
273}
274
276{
277 if(
278 src_type.id() != ID_struct_tag &&
279 src_type.id() != ID_union_tag)
280 {
281 return src_type;
282 }
283
284 typet result_type=src_type;
285
286 // collect qualifiers
288
289 if(
291 {
292 const typet &followed_type = ns.follow_tag(*struct_tag_type);
293 result_type = followed_type;
295 }
296 else if(
298 {
299 const typet &followed_type = ns.follow_tag(*union_tag_type);
300 result_type = followed_type;
302 }
303
304 qualifiers.write(result_type);
305
306 return result_type;
307}
308
310 const typet &type) const
311{
312 if(type.id()==ID_signedbv)
313 {
314 const std::size_t width = to_bitvector_type(type).get_width();
315
316 if(width<=config.ansi_c.char_width)
317 return CHAR;
318 else if(width<=config.ansi_c.short_int_width)
319 return SHORT;
320 else if(width<=config.ansi_c.int_width)
321 return INT;
322 else if(width<=config.ansi_c.long_int_width)
323 return LONG;
324 else if(width<=config.ansi_c.long_long_int_width)
325 return LONGLONG;
326 else
327 return LARGE_SIGNED_INT;
328 }
329 else if(type.id()==ID_unsignedbv)
330 {
331 const std::size_t width = to_bitvector_type(type).get_width();
332
333 if(width<=config.ansi_c.char_width)
334 return UCHAR;
335 else if(width<=config.ansi_c.short_int_width)
336 return USHORT;
337 else if(width<=config.ansi_c.int_width)
338 return UINT;
339 else if(width<=config.ansi_c.long_int_width)
340 return ULONG;
341 else if(width<=config.ansi_c.long_long_int_width)
342 return ULONGLONG;
343 else
344 return LARGE_UNSIGNED_INT;
345 }
346 else if(type.id()==ID_bool)
347 return BOOL;
348 else if(type.id()==ID_c_bool)
349 return BOOL;
350 else if(type.id()==ID_floatbv)
351 {
352 const std::size_t width = to_bitvector_type(type).get_width();
353
354 if(width<=config.ansi_c.single_width)
355 return SINGLE;
356 else if(width<=config.ansi_c.double_width)
357 return DOUBLE;
358 else if(width<=config.ansi_c.long_double_width)
359 return LONGDOUBLE;
360 else if(width<=128)
361 return FLOAT128;
362 }
363 else if(type.id()==ID_fixedbv)
364 {
365 return FIXEDBV;
366 }
367 else if(type.id()==ID_pointer)
368 {
369 if(to_pointer_type(type).base_type().id() == ID_empty)
370 return VOIDPTR;
371 else
372 return PTR;
373 }
374 else if(type.id()==ID_array)
375 {
376 return PTR;
377 }
378 else if(type.id() == ID_c_enum || type.id() == ID_c_enum_tag)
379 {
380 return INT;
381 }
382 else if(type.id()==ID_rational)
383 return RATIONAL;
384 else if(type.id()==ID_real)
385 return REAL;
386 else if(type.id()==ID_complex)
387 return COMPLEX;
388 else if(type.id()==ID_c_bit_field)
389 {
390 const auto &bit_field_type = to_c_bit_field_type(type);
391
392 // We take the underlying type, and then apply the number
393 // of bits given
394 typet underlying_type;
395
396 if(bit_field_type.underlying_type().id() == ID_c_enum_tag)
397 {
398 const auto &followed =
399 ns.follow_tag(to_c_enum_tag_type(bit_field_type.underlying_type()));
400 if(followed.is_incomplete())
401 return INT;
402 else
403 underlying_type = followed.underlying_type();
404 }
405 else
406 underlying_type = bit_field_type.underlying_type();
407
409 underlying_type.id(), bit_field_type.get_width());
410
411 return get_c_type(new_type);
412 }
413 else if(type.id() == ID_integer)
414 return INTEGER;
415 else if(type.id() == ID_natural)
416 return NATURAL;
417
418 return OTHER;
419}
420
422 exprt &expr,
424{
426
427 switch(c_type)
428 {
429 case PTR:
430 if(expr.type().id() == ID_array)
431 {
432 new_type = pointer_type(to_array_type(expr.type()).element_type());
433 break;
434 }
435 return;
436
437 case BOOL: UNREACHABLE; // should always be promoted to int
438 case CHAR: UNREACHABLE; // should always be promoted to int
439 case UCHAR: UNREACHABLE; // should always be promoted to int
440 case SHORT: UNREACHABLE; // should always be promoted to int
441 case USHORT: UNREACHABLE; // should always be promoted to int
442 case INT: new_type=signed_int_type(); break;
443 case UINT: new_type=unsigned_int_type(); break;
444 case LONG: new_type=signed_long_int_type(); break;
448 case SINGLE: new_type=float_type(); break;
449 case DOUBLE: new_type=double_type(); break;
450 case LONGDOUBLE: new_type=long_double_type(); break;
451 // NOLINTNEXTLINE(whitespace/line_length)
453 case RATIONAL: new_type=rational_typet(); break;
454 case REAL: new_type=real_typet(); break;
455 case INTEGER: new_type=integer_typet(); break;
456 case NATURAL:
458 break;
459 case COMPLEX:
460 case OTHER:
461 case VOIDPTR:
462 case FIXEDBV:
464 case LARGE_SIGNED_INT:
465 return; // do nothing
466 }
467
468 if(new_type != expr.type())
469 do_typecast(expr, new_type);
470}
471
473 const typet &type) const
474{
476
477 // 6.3.1.1, par 2
478
479 // "If an int can represent all values of the original type, the
480 // value is converted to an int; otherwise, it is converted to
481 // an unsigned int."
482
483 c_typet max_type=std::max(c_type, INT); // minimum promotion
484
485 // The second case can arise if we promote any unsigned type
486 // that is as large as unsigned int. In this case the promotion configuration
487 // via the enum is actually wrong, and we need to fix this up.
488 if(
489 config.ansi_c.short_int_width == config.ansi_c.int_width &&
490 c_type == USHORT)
492 else if(
493 config.ansi_c.char_width == config.ansi_c.int_width && c_type == UCHAR)
495
496 if(max_type==UINT &&
497 type.id()==ID_c_bit_field &&
498 to_c_bit_field_type(type).get_width()<config.ansi_c.int_width)
500
501 return max_type;
502}
503
509
523
525 exprt &expr,
526 const typet &src_type,
527 const typet &orig_dest_type,
528 const typet &dest_type)
529{
530 // do transparent union
531 if(dest_type.id()==ID_union &&
533 src_type.id()!=ID_union)
534 {
535 // The argument corresponding to a transparent union type can be of any
536 // type in the union; no explicit cast is required.
537
538 // GCC docs say:
539 // If the union member type is a pointer, qualifiers like const on the
540 // referenced type must be respected, just as with normal pointer
541 // conversions.
542 // But it is accepted, and Clang doesn't even emit a warning (GCC 4.7 does)
544 if(
545 src_type.id() == ID_pointer &&
546 to_pointer_type(src_type).base_type().get_bool(ID_C_constant))
547 {
549 }
550
551 // Check union members.
552 for(const auto &comp : to_union_type(dest_type).components())
553 {
555 {
556 // build union constructor
557 union_exprt union_expr(comp.get_name(), expr, orig_dest_type);
558 if(!src_type.full_eq(src_type_no_const))
560 expr=union_expr;
561 return; // ok
562 }
563 }
564 }
565
566 if(dest_type.id()==ID_pointer)
567 {
568 // special case: 0 == NULL
569
570 if(
571 simplify_expr(expr, ns) == 0 &&
572 (src_type.id() == ID_unsignedbv || src_type.id() == ID_signedbv ||
573 src_type.id() == ID_natural || src_type.id() == ID_integer))
574 {
576 return; // ok
577 }
578
579 if(src_type.id()==ID_pointer ||
580 src_type.id()==ID_array)
581 {
582 // we are quite generous about pointers
583
584 const typet &src_sub = to_type_with_subtype(src_type).subtype();
585 const typet &dest_sub = to_pointer_type(dest_type).base_type();
586
588 {
589 // from/to void is always good
590 }
591 else if(src_sub.id()==ID_code &&
592 dest_sub.id()==ID_code)
593 {
594 // very generous:
595 // between any two function pointers it's ok
596 }
597 else if(src_sub == dest_sub)
598 {
599 // ok
600 }
601 else if((is_number(src_sub) ||
602 src_sub.id()==ID_c_enum ||
603 src_sub.id()==ID_c_enum_tag) &&
605 dest_sub.id()==ID_c_enum ||
606 src_sub.id()==ID_c_enum_tag))
607 {
608 // Also generous: between any to scalar types it's ok.
609 // We should probably check the size.
610 }
611 else if(
612 src_sub.id() == ID_array && dest_sub.id() == ID_array &&
613 to_array_type(src_sub).element_type() ==
614 to_array_type(dest_sub).element_type())
615 {
616 // we ignore the size of the top-level array
617 // in the case of pointers to arrays
618 }
619 else
620 warnings.push_back("incompatible pointer types");
621
622 // check qualifiers
623
624 if(
625 to_type_with_subtype(src_type).subtype().get_bool(ID_C_volatile) &&
626 !to_pointer_type(dest_type).base_type().get_bool(ID_C_volatile))
627 {
628 warnings.push_back("disregarding volatile");
629 }
630
632 {
633 expr.type()=src_type; // because of qualifiers
634 }
635 else
637
638 return; // ok
639 }
640 }
641
643 errors.push_back("implicit conversion not permitted");
644 else if(src_type!=dest_type)
646}
647
649 exprt &expr1,
650 exprt &expr2)
651{
652 const typet &type1 = expr1.type();
653 const typet &type2 = expr2.type();
654
657
658 c_typet max_type=std::max(c_type1, c_type2);
659
661 {
662 // produce type
663 typet result_type = (max_type == c_type1) ? type1 : type2;
664
665 do_typecast(expr1, result_type);
666 do_typecast(expr2, result_type);
667
668 return;
669 }
670 else if(max_type==FIXEDBV)
671 {
672 typet result_type;
673
675 {
676 // get bigger of both
677 std::size_t width1=to_fixedbv_type(type1).get_width();
678 std::size_t width2=to_fixedbv_type(type2).get_width();
679 if(width1>=width2)
680 result_type=type1;
681 else
682 result_type=type2;
683 }
684 else if(c_type1==FIXEDBV)
685 result_type=type1;
686 else
687 result_type=type2;
688
689 do_typecast(expr1, result_type);
690 do_typecast(expr2, result_type);
691
692 return;
693 }
694 else if(max_type==COMPLEX)
695 {
697 {
698 // promote to the one with bigger subtype
699 if(
700 get_c_type(to_complex_type(type1).subtype()) >
701 get_c_type(to_complex_type(type2).subtype()))
702 {
704 }
705 else
707 }
708 else if(c_type1==COMPLEX)
709 {
710 INVARIANT(c_type2 != COMPLEX, "both types were COMPLEX");
713 }
714 else
715 {
716 INVARIANT(c_type2 == COMPLEX, "neither type was COMPLEX");
719 }
720
721 return;
722 }
723 else if(max_type==SINGLE || max_type==DOUBLE ||
725 {
726 // Special-case optimisation:
727 // If we have two non-standard sized floats, don't do implicit type
728 // promotion if we can possibly avoid it.
729 if(type1==type2)
730 return;
731 }
732 else if(max_type == OTHER)
733 {
734 errors.push_back("implicit arithmetic conversion not permitted");
735 return;
736 }
737
740}
741
743{
744 // special case: array -> pointer is actually
745 // something like address_of
746
747 const typet &src_type = expr.type();
748
749 if(src_type.id()==ID_array)
750 {
751 // This is the promotion from an array
752 // to a pointer to the first element.
754 if(error_opt.has_value())
755 {
756 errors.push_back(error_opt.value());
757 return;
758 }
759
760 index_exprt index(expr, from_integer(0, c_index_type()));
762 return;
763 }
764
766 {
767 // C booleans are special; we produce the
768 // explicit comparison with zero.
769 // Note that this requires ieee_float_notequal
770 // in case of floating-point numbers.
771
773 {
774 expr = typecast_exprt(is_not_zero(expr, ns), dest_type);
775 }
776 else if(dest_type.id()==ID_bool)
777 {
778 expr=is_not_zero(expr, ns);
779 }
780 else if(dest_type.id() == ID_rational)
781 {
783 {
784 auto op1 = numeric_cast<mp_integer>(div_expr->lhs());
785 auto op2 = numeric_cast<mp_integer>(div_expr->rhs());
786 if(op1.has_value() && op2.has_value())
787 {
788 rationalt numerator{*op1};
789 expr = from_rational(rationalt{*op1} / rationalt{*op2});
790 return;
791 }
792 }
793 else if(auto int_const = numeric_cast<mp_integer>(expr))
794 {
796 return;
797 }
798
799 expr = typecast_exprt(expr, dest_type);
800 }
801 else
802 {
803 expr = typecast_exprt(expr, dest_type);
804 }
805 }
806}
807
808std::optional<std::string>
810{
811 if(type.id() == ID_c_bit_field)
812 return std::string("cannot take address of a bit field");
813
814 if(type.id() == ID_bool)
815 return std::string("cannot take address of a proper Boolean");
816
818 {
819 // The width of the bitvector must be a multiple of CHAR_BIT.
820 auto width = to_bitvector_type(type).get_width();
821 if(width % config.ansi_c.char_width != 0)
822 {
823 return std::string(
824 "bitvector must have width that is a multiple of CHAR_BIT");
825 }
826 else
827 return {};
828 }
829
830 if(type.id() == ID_array)
831 return check_address_can_be_taken(to_array_type(type).element_type());
832
833 return {}; // ok
834}
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:177
signedbv_typet signed_long_int_type()
Definition c_types.cpp:72
unsignedbv_typet unsigned_int_type()
Definition c_types.cpp:36
unsignedbv_typet unsigned_long_long_int_type()
Definition c_types.cpp:93
unsignedbv_typet unsigned_long_int_type()
Definition c_types.cpp:86
signedbv_typet signed_int_type()
Definition c_types.cpp:22
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:235
signedbv_typet signed_long_long_int_type()
Definition c_types.cpp:79
floatbv_typet long_double_type()
Definition c_types.cpp:193
bitvector_typet c_index_type()
Definition c_types.cpp:16
floatbv_typet double_type()
Definition c_types.cpp:185
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.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Base class of fixed-width bit-vector types.
Definition std_types.h:909
@ LARGE_UNSIGNED_INT
Definition c_typecast.h:92
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)
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:67
const namespacet & ns
Definition c_typecast.h:74
static std::optional< std::string > check_address_can_be_taken(const typet &)
c_typet minimum_promotion(const typet &type) const
std::list< std::string > errors
Definition c_typecast.h:66
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:38
Base class for all expressions.
Definition expr.h:57
typet & type()
Return the type of the expression.
Definition expr.h:85
static ieee_float_spect quadruple_precision()
Definition ieee_float.h:82
Array index operator.
Definition std_expr.h:1470
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:364
const irep_idt & id() const
Definition irep.h:388
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Natural numbers including zero (mathematical integers, not bitvectors)
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.
Semantic type conversion.
Definition std_expr.h:2073
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2081
The type of an expression, extends irept.
Definition type.h:29
Union constructor from single element.
Definition std_expr.h:1770
exprt is_not_zero(const exprt &src, const namespacet &ns)
converts a scalar/float expression to C/C++ Booleans
Definition expr_util.cpp:69
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.
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
constant_exprt from_rational(const rationalt &a)
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:1158
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:888
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition type.h:208