CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
cpp_typecheck_conversions.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: C++ Language Type Checking
4
5Author:
6
7\*******************************************************************/
8
11
12#include "cpp_typecheck.h"
13
14#include <util/arith_tools.h>
15#include <util/c_types.h>
16#include <util/config.h>
17#include <util/expr_util.h>
18#include <util/pointer_expr.h>
19#include <util/simplify_expr.h>
20#include <util/std_expr.h>
21
22#include <ansi-c/c_qualifiers.h>
23
24#include "cpp_util.h"
25
47 const exprt &expr,
48 exprt &new_expr) const
49{
51
52 if(expr.type().id() == ID_code)
53 return false;
54
55 if(
56 expr.type().id() == ID_struct &&
57 to_struct_type(expr.type()).is_incomplete())
58 return false;
59
60 if(expr.type().id() == ID_union && to_union_type(expr.type()).is_incomplete())
61 return false;
62
63 new_expr=expr;
64 new_expr.remove(ID_C_lvalue);
65
66 return true;
67}
68
78 const exprt &expr,
79 exprt &new_expr) const
80{
81 PRECONDITION(expr.type().id() == ID_array);
82
83 index_exprt index(expr, from_integer(0, c_index_type()));
84
85 index.set(ID_C_lvalue, true);
86
88
89 return true;
90}
91
100 const exprt &expr, exprt &new_expr) const
101{
102 if(!expr.get_bool(ID_C_lvalue))
103 return false;
104
106
107 return true;
108}
109
116 const exprt &expr,
117 const typet &type,
118 exprt &new_expr) const
119{
120 if(expr.type().id()!=ID_pointer ||
121 is_reference(expr.type()))
122 return false;
123
124 if(expr.get_bool(ID_C_lvalue))
125 return false;
126
127 if(expr.type()!=type)
128 return false;
129
130 typet sub_from = to_pointer_type(expr.type()).base_type();
131 typet sub_to = to_pointer_type(type).base_type();
132 bool const_to=true;
133
134 while(sub_from.id()==ID_pointer)
135 {
138
139 if(!qual_to.is_constant)
140 const_to=false;
141
142 if(qual_from.is_constant && !qual_to.is_constant)
143 return false;
144
145 if(qual_from!=qual_to && !const_to)
146 return false;
147
148 typet tmp1 = to_pointer_type(sub_from).base_type();
149 sub_from.swap(tmp1);
150
151 typet tmp2 = sub_to.add_subtype();
152 sub_to.swap(tmp2);
153 }
154
157
158 if(qual_from.is_subset_of(qual_to))
159 {
160 new_expr=expr;
161 new_expr.type()=type;
162 return true;
163 }
164
165 return false;
166}
167
194 const exprt &expr,
195 exprt &new_expr) const
196{
197 if(expr.get_bool(ID_C_lvalue))
198 return false;
199
201 qual_from.read(expr.type());
202
204 qual_from.write(int_type);
205
206 if(expr.type().id()==ID_signedbv)
207 {
208 std::size_t width=to_signedbv_type(expr.type()).get_width();
209 if(width >= config.ansi_c.int_width)
210 return false;
212 return true;
213 }
214
215 if(expr.type().id()==ID_unsignedbv)
216 {
217 std::size_t width=to_unsignedbv_type(expr.type()).get_width();
218 if(width >= config.ansi_c.int_width)
219 return false;
221 return true;
222 }
223
224 if(expr.is_boolean() || expr.type().id() == ID_c_bool)
225 {
227 return true;
228 }
229
230 if(expr.type().id()==ID_c_enum_tag)
231 {
233 return true;
234 }
235
236 return false;
237}
238
247 const exprt &expr,
248 exprt &new_expr) const
249{
250 if(expr.get_bool(ID_C_lvalue))
251 return false;
252
253 // we only do that with 'float',
254 // not with 'double' or 'long double'
255 if(expr.type()!=float_type())
256 return false;
257
258 std::size_t width=to_floatbv_type(expr.type()).get_width();
259
260 if(width!=config.ansi_c.single_width)
261 return false;
262
264 qual_from.read(expr.type());
265
267 qual_from.write(new_expr.type());
268
269 return true;
270}
271
301 const exprt &expr,
302 const typet &type,
303 exprt &new_expr) const
304{
305 if(type.id()!=ID_signedbv &&
306 type.id()!=ID_unsignedbv)
307 return false;
308
309 if(
310 expr.type().id() != ID_signedbv && expr.type().id() != ID_unsignedbv &&
311 expr.type().id() != ID_c_bool && !expr.is_boolean() &&
312 expr.type().id() != ID_c_enum_tag)
313 {
314 return false;
315 }
316
317 if(expr.get_bool(ID_C_lvalue))
318 return false;
319
321 qual_from.read(expr.type());
323 qual_from.write(new_expr.type());
324
325 return true;
326}
327
348 const exprt &expr,
349 const typet &type,
350 exprt &new_expr) const
351{
352 if(expr.get_bool(ID_C_lvalue))
353 return false;
354
355 if(expr.type().id()==ID_floatbv ||
356 expr.type().id()==ID_fixedbv)
357 {
358 if(type.id()!=ID_signedbv &&
359 type.id()!=ID_unsignedbv)
360 return false;
361 }
362 else if(expr.type().id()==ID_signedbv ||
363 expr.type().id()==ID_unsignedbv ||
364 expr.type().id()==ID_c_enum_tag)
365 {
366 if(type.id()!=ID_fixedbv &&
367 type.id()!=ID_floatbv)
368 return false;
369 }
370 else
371 return false;
372
374 qual_from.read(expr.type());
376 qual_from.write(new_expr.type());
377
378 return true;
379}
380
381
399 const exprt &expr,
400 const typet &type,
401 exprt &new_expr) const
402{
403 if(expr.type().id()!=ID_floatbv &&
404 expr.type().id()!=ID_fixedbv)
405 return false;
406
407 if(type.id()!=ID_floatbv &&
408 type.id()!=ID_fixedbv)
409 return false;
410
411 if(expr.get_bool(ID_C_lvalue))
412 return false;
413
415
416 qual_from.read(expr.type());
418 qual_from.write(new_expr.type());
419
420 return true;
421}
422
456 const exprt &expr,
457 const typet &type,
459{
460 if(type.id()!=ID_pointer ||
461 is_reference(type))
462 return false;
463
464 if(expr.get_bool(ID_C_lvalue))
465 return false;
466
467 // integer 0 to NULL pointer conversion?
468 if(simplify_expr(expr, *this).is_zero() &&
469 expr.type().id()!=ID_pointer)
470 {
471 new_expr=expr;
473 new_expr.type()=type;
474 return true;
475 }
476
477 if(type.find(ID_to_member).is_not_nil())
478 return false;
479
480 if(
481 expr.type().id() != ID_pointer ||
482 expr.type().find(ID_to_member).is_not_nil())
483 {
484 return false;
485 }
486
488 const typet &sub_from = to_pointer_type(expr.type()).base_type();
490
491 // std::nullptr_t to _any_ pointer type
492 if(sub_from.id()==ID_nullptr)
493 return true;
494
495 // anything but function pointer to void *
496 if(sub_from.id()!=ID_code && sub_to.id()==ID_empty)
497 {
499 qual_from.read(to_pointer_type(expr.type()).base_type());
501 qual_from.write(to_pointer_type(new_expr.type()).base_type());
502 return true;
503 }
504
505 // struct * to struct *
506 if(sub_from.id() == ID_struct_tag && sub_to.id() == ID_struct_tag)
507 {
511 {
513 qual_from.read(to_pointer_type(expr.type()).base_type());
514 new_expr=expr;
516 qual_from.write(to_pointer_type(new_expr.type()).base_type());
517 return true;
518 }
519 }
520
521 return false;
522}
523
555 const exprt &expr,
556 const typet &type,
558{
559 if(
560 type.id() != ID_pointer || is_reference(type) ||
561 type.find(ID_to_member).is_nil())
562 {
563 return false;
564 }
565
566 if(expr.type().id() != ID_pointer || expr.type().find(ID_to_member).is_nil())
567 return false;
568
569 if(
570 to_pointer_type(type).base_type() !=
571 to_pointer_type(expr.type()).base_type())
572 {
573 // base types are different
574 if(
575 to_pointer_type(type).base_type().id() == ID_code &&
576 to_pointer_type(expr.type()).base_type().id() == ID_code)
577 {
578 code_typet code1 = to_code_type(to_pointer_type(expr.type()).base_type());
579 DATA_INVARIANT(!code1.parameters().empty(), "must have parameters");
580 code_typet::parametert this1=code1.parameters()[0];
581 INVARIANT(this1.get_this(), "first parameter should be `this'");
582 code1.parameters().erase(code1.parameters().begin());
583
584 code_typet code2 = to_code_type(to_pointer_type(type).base_type());
585 DATA_INVARIANT(!code2.parameters().empty(), "must have parameters");
586 code_typet::parametert this2=code2.parameters()[0];
587 INVARIANT(this2.get_this(), "first parameter should be `this'");
588 code2.parameters().erase(code2.parameters().begin());
589
590 if(
591 to_pointer_type(this2.type()).base_type().get_bool(ID_C_constant) &&
592 !to_pointer_type(this1.type()).base_type().get_bool(ID_C_constant))
593 return false;
594
595 // give a second chance ignoring `this'
596 if(code1!=code2)
597 return false;
598 }
599 else
600 return false;
601 }
602
603 if(expr.get_bool(ID_C_lvalue))
604 return false;
605
606 if(expr.is_constant() && to_constant_expr(expr).is_null_pointer())
607 {
609 return true;
610 }
611
613 static_cast<const typet &>(expr.type().find(ID_to_member))));
614
616 to_struct_tag_type(static_cast<const typet &>(type.find(ID_to_member))));
617
619 {
621 return true;
622 }
623
624 return false;
625}
626
637 const exprt &expr, exprt &new_expr) const
638{
639 if(expr.get_bool(ID_C_lvalue))
640 return false;
641
642 if(
643 expr.type().id() != ID_signedbv && expr.type().id() != ID_unsignedbv &&
644 expr.type().id() != ID_pointer && !expr.is_boolean() &&
645 expr.type().id() != ID_c_enum_tag)
646 {
647 return false;
648 }
649
651 qual_from.read(expr.type());
652
654 qual_from.write(Bool);
655
657 return true;
658}
659
681 const exprt &expr,
682 const typet &type,
684 unsigned &rank)
685{
686 PRECONDITION(!is_reference(expr.type()) && !is_reference(type));
687
688 exprt curr_expr=expr;
689
690 // bit fields are converted like their underlying type
691 if(type.id()==ID_c_bit_field)
693 expr, to_c_bit_field_type(type).underlying_type(), new_expr, rank);
694
695 // we turn bit fields into their underlying type
696 if(curr_expr.type().id()==ID_c_bit_field)
698 curr_expr, to_c_bit_field_type(curr_expr.type()).underlying_type());
699
700 if(curr_expr.type().id()==ID_array)
701 {
702 if(type.id()==ID_pointer)
703 {
705 return false;
706 }
707 }
708 else if(curr_expr.type().id()==ID_code &&
709 type.id()==ID_pointer)
710 {
712 return false;
713 }
714 else if(curr_expr.get_bool(ID_C_lvalue))
715 {
717 return false;
718 }
719 else
721
722 curr_expr.swap(new_expr);
723
724 // two enums are the same if the tag is the same,
725 // even if the width differs (enum bit-fields!)
726 if(type.id() == ID_c_enum_tag && curr_expr.type().id() == ID_c_enum_tag)
727 {
728 if(
729 to_tag_type(type).get_identifier() ==
730 to_tag_type(curr_expr.type()).get_identifier())
731 {
732 return true;
733 }
734 else
735 {
736 // In contrast to C, we simply don't allow implicit conversions
737 // between enums.
738 return false;
739 }
740 }
741
742 // need to consider #c_type
743 if(
744 curr_expr.type() != type ||
745 curr_expr.type().get(ID_C_c_type) != type.get(ID_C_c_type))
746 {
747 if(
748 type.id() == ID_signedbv || type.id() == ID_unsignedbv ||
749 type.id() == ID_c_enum_tag)
750 {
752 new_expr.type() != type)
753 {
755 {
757 curr_expr, type, new_expr))
758 return false;
759 }
760
761 rank+=3;
762 }
763 else
764 rank+=2;
765 }
766 else if(type.id()==ID_floatbv || type.id()==ID_fixedbv)
767 {
769 new_expr.type() != type)
770 {
772 curr_expr, type, new_expr) &&
774 curr_expr, type, new_expr))
775 return false;
776
777 rank += 3;
778 }
779 else
780 rank += 2;
781 }
782 else if(type.id()==ID_pointer)
783 {
784 if(
785 expr.type().id() == ID_pointer &&
786 to_pointer_type(expr.type()).base_type().id() == ID_nullptr)
787 {
788 // std::nullptr_t to _any_ pointer type is ok
790 }
792 {
794 return false;
795 }
796
797 rank += 3;
798 }
799 else if(type.id() == ID_c_bool)
800 {
802 return false;
803
804 rank += 3;
805 }
806 else if(type.id() == ID_bool)
807 {
809
810 rank += 3;
811 }
812 else
813 return false;
814 }
815 else
817
818 curr_expr.swap(new_expr);
819
820 if(curr_expr.type().id()==ID_pointer)
821 {
822 typet sub_from=curr_expr.type();
823 typet sub_to=type;
824
825 do
826 {
827 typet tmp_from = to_pointer_type(sub_from).base_type();
828 sub_from.swap(tmp_from);
829 typet tmp_to = sub_to.add_subtype();
830 sub_to.swap(tmp_to);
831
833 qual_from.read(sub_from);
834
836 qual_to.read(sub_to);
837
838 if(qual_from!=qual_to)
839 {
840 rank+=1;
841 break;
842 }
843 }
844 while(sub_from.id()==ID_pointer);
845
847 return false;
848 }
849 else
850 {
852 new_expr.type()=type;
853 }
854
855 return true;
856}
857
864 const exprt &expr,
865 const typet &to,
867 unsigned &rank)
868{
871
872 const typet &from = expr.type();
873
874 new_expr.make_nil();
875
876 // special case:
877 // A conversion from a type to the same type is given an exact
878 // match rank even though a user-defined conversion is used
879
880 if(from==to)
881 rank+=0;
882 else
883 rank+=4; // higher than all the standard conversions
884
885 if(to.id() == ID_struct_tag)
886 {
887 std::string err_msg;
888
889 if(cpp_is_pod(to))
890 {
891 if(from.id() == ID_struct_tag)
892 {
895
896 // potentially requires
897 // expr.get_bool(ID_C_lvalue) ??
898
900 {
901 exprt address=address_of_exprt(expr);
902
903 // simplify address
904 if(expr.id()==ID_dereference)
905 address = to_dereference_expr(expr).pointer();
906
909 qual_from.read(expr.type());
910 qual_from.write(ptr_sub.base_type());
911 make_ptr_typecast(address, ptr_sub);
912
913 const dereference_exprt deref(address);
914
915 // create temporary object
918 tmp_object_expr.copy_to_operands(deref);
919 tmp_object_expr.set(ID_C_lvalue, true);
921
923 return true;
924 }
925 }
926 }
927 else
928 {
929 bool found=false;
931
932 for(const auto &component : struct_type_to.components())
933 {
934 if(component.get_bool(ID_from_base))
935 continue;
936
937 if(component.get_bool(ID_is_explicit))
938 continue;
939
940 const typet &comp_type = component.type();
941
942 if(comp_type.id() !=ID_code)
943 continue;
944
945 if(to_code_type(comp_type).return_type().id() != ID_constructor)
946 continue;
947
948 // TODO: ellipsis
949
950 const auto &parameters = to_code_type(comp_type).parameters();
951
952 if(parameters.size() != 2)
953 continue;
954
955 exprt curr_arg1 = parameters[1];
957
959 {
960 typet tmp = to_reference_type(arg1_type).base_type();
961 arg1_type.swap(tmp);
962 }
963
964 unsigned tmp_rank=0;
965 if(arg1_type.id() != ID_struct_tag)
966 {
969 expr, arg1_type, tmp_expr, tmp_rank))
970 {
971 // check if it's ambiguous
972 if(found)
973 return false;
974 found=true;
975
976 if(expr.get_bool(ID_C_lvalue))
977 tmp_expr.set(ID_C_lvalue, true);
978
979 tmp_expr.add_source_location()=expr.source_location();
980
982 func_symb.type()=comp_type;
984
985 // create temporary object
987 std::move(func_symb),
988 {tmp_expr},
990 expr.source_location());
993
994 new_expr.swap(ctor_expr);
995
996 if(struct_type_to.get_bool(ID_C_constant))
997 new_expr.type().set(ID_C_constant, true);
998
999 rank += tmp_rank;
1000 }
1001 }
1002 else if(from.id() == ID_struct_tag && arg1_type.id() == ID_struct_tag)
1003 {
1004 // try derived-to-base conversion
1007
1009 tmp_rank=0;
1012 {
1013 // check if it's ambiguous
1014 if(found)
1015 return false;
1016 found=true;
1017
1018 rank+=tmp_rank;
1019
1020 // create temporary object
1022 expr_deref.set(ID_C_lvalue, true);
1023 expr_deref.add_source_location()=expr.source_location();
1024
1026 new_object.set(ID_C_lvalue, true);
1027 new_object.type().set(ID_C_constant, false);
1028
1030 func_symb.type()=comp_type;
1032
1034 std::move(func_symb),
1035 {expr_deref},
1037 expr.source_location());
1039
1040 new_expr.swap(ctor_expr);
1041
1042 INVARIANT(
1044 "statement ID");
1045
1046 if(struct_type_to.get_bool(ID_C_constant))
1047 new_expr.type().set(ID_C_constant, true);
1048 }
1049 }
1050 }
1051 if(found)
1052 return true;
1053 }
1054 }
1055
1056 // conversion operators
1057 if(from.id() == ID_struct_tag)
1058 {
1059 bool found=false;
1060 for(const auto &component :
1061 follow_tag(to_struct_tag_type(from)).components())
1062 {
1063 if(component.get_bool(ID_from_base))
1064 continue;
1065
1066 if(!component.get_bool(ID_is_cast_operator))
1067 continue;
1068
1069 const code_typet &comp_type = to_code_type(component.type());
1071 comp_type.parameters().size() == 1, "expected exactly one parameter");
1072
1073 typet this_type = comp_type.parameters().front().type();
1074 this_type.set(ID_C_reference, true);
1075
1076 exprt this_expr(expr);
1077 this_type.set(ID_C_this, true);
1078
1079 unsigned tmp_rank=0;
1081
1083 this_expr, this_type, tmp_expr, tmp_rank))
1084 {
1085 // To take care of the possible virtual case,
1086 // we build the function as a member expression.
1087 const cpp_namet cpp_func_name(component.get_base_name());
1088
1091 member_func.copy_to_operands(already_typechecked_exprt{expr});
1092
1094 std::move(member_func),
1095 {},
1097 expr.source_location());
1099
1101 {
1102 // check if it's ambiguous
1103 if(found)
1104 return false;
1105 found=true;
1106
1107 rank+=tmp_rank;
1108 new_expr.swap(tmp_expr);
1109 }
1110 }
1111 }
1112 if(found)
1113 return true;
1114 }
1115
1116 return new_expr.is_not_nil();
1117}
1118
1124 const exprt &expr,
1125 const reference_typet &reference_type) const
1126{
1127 PRECONDITION(!is_reference(expr.type()));
1128
1129 const typet &from = expr.type();
1130 const typet &from_followed =
1131 from.id() == ID_struct_tag
1132 ? static_cast<const typet &>(follow_tag(to_struct_tag_type(from)))
1133 : from.id() == ID_union_tag
1134 ? static_cast<const typet &>(follow_tag(to_union_tag_type(from)))
1135 : from;
1136 const typet &to = reference_type.base_type();
1137 const typet &to_followed =
1138 to.id() == ID_struct_tag
1139 ? static_cast<const typet &>(follow_tag(to_struct_tag_type(to)))
1140 : to.id() == ID_union_tag
1141 ? static_cast<const typet &>(follow_tag(to_union_tag_type(to)))
1142 : to;
1143
1144 // need to check #c_type
1146 return false;
1147
1148 if(from==to)
1149 return true;
1150
1151 if(from.id() == ID_struct_tag && to.id() == ID_struct_tag)
1152 {
1153 return subtype_typecast(
1155 }
1156
1157 if(
1159 to.id() == ID_empty)
1160 {
1161 // virtual-call case
1162 return true;
1163 }
1164
1165 return false;
1166}
1167
1173 const exprt &expr,
1175 unsigned &rank) const
1176{
1177 PRECONDITION(!is_reference(expr.type()));
1178
1180 return false;
1181
1182 if(expr.type() != reference_type.base_type())
1183 rank+=3;
1184
1186 qual_from.read(expr.type());
1187
1190
1191 if(qual_from!=qual_to)
1192 rank+=1;
1193
1194 if(qual_from.is_subset_of(qual_to))
1195 return true;
1196
1197 return false;
1198}
1199
1235 exprt expr,
1237 exprt &new_expr,
1238 unsigned &rank)
1239{
1240 PRECONDITION(!is_reference(expr.type()));
1241
1242 unsigned backup_rank=rank;
1243
1245 {
1246 // `this' has to be an lvalue
1248 expr.set(ID_C_lvalue, true);
1249 else if(expr.get(ID_statement)==ID_function_call)
1250 expr.set(ID_C_lvalue, true);
1251 else if(expr.get_bool(ID_C_temporary_avoided))
1252 {
1255 new_temporary(expr.source_location(), expr.type(), expr, temporary);
1256 expr.swap(temporary);
1257 expr.set(ID_C_lvalue, true);
1258 }
1259 else
1260 return false;
1261 }
1262
1263 if(
1264 expr.get_bool(ID_C_lvalue) ||
1266 {
1268 {
1269 if(!expr.get_bool(ID_C_lvalue))
1270 {
1271 // create temporary object
1274 {std::move(expr)},
1276 expr.source_location()};
1277 tmp.set(ID_mode, ID_cpp);
1278 expr.swap(tmp);
1279 }
1280
1281 {
1283 tmp.add_source_location()=expr.source_location();
1284 new_expr.swap(tmp);
1285 }
1286
1287 if(expr.type() != reference_type.base_type())
1288 {
1290 qual_from.read(expr.type());
1292 qual_from.write(to_reference_type(new_expr.type()).base_type());
1293 }
1294
1295 return true;
1296 }
1297
1299 }
1300
1301 // conversion operators
1302 if(expr.type().id() == ID_struct_tag)
1303 {
1304 for(const auto &component :
1305 follow_tag(to_struct_tag_type(expr.type())).components())
1306 {
1307 if(component.get_bool(ID_from_base))
1308 continue;
1309
1310 if(!component.get_bool(ID_is_cast_operator))
1311 continue;
1312
1313 const code_typet &component_type = to_code_type(component.type());
1314
1315 // otherwise it cannot bind directly (not an lvalue)
1316 if(!is_reference(component_type.return_type()))
1317 continue;
1318
1320 component_type.parameters().size() == 1, "exactly one parameter");
1321
1323 component_type.parameters().front().type();
1324 this_type.set(ID_C_reference, true);
1325
1326 exprt this_expr(expr);
1327
1328 this_type.set(ID_C_this, true);
1329
1330 unsigned tmp_rank=0;
1331
1334 this_expr, this_type, tmp_expr, tmp_rank))
1335 {
1336 // To take care of the possible virtual case,
1337 // we build the function as a member expression.
1338 const cpp_namet cpp_func_name(component.get_base_name());
1339
1342 member_func.copy_to_operands(already_typechecked_exprt{expr});
1343
1345 std::move(member_func),
1346 {},
1348 expr.source_location());
1350
1351 // let's check if the returned value binds directly
1354
1355 if(
1356 returned_value.get_bool(ID_C_lvalue) &&
1358 {
1359 // returned values are lvalues in case of references only
1362 "the returned value must be pointer to reference");
1363
1365
1367 {
1369 qual_from.read(returned_value.type());
1371 qual_from.write(to_reference_type(new_expr.type()).base_type());
1372 }
1373 rank+=4+tmp_rank;
1374 return true;
1375 }
1376 }
1377 }
1378 }
1379
1380 // No temporary allowed for `this'
1382 return false;
1383
1384 if(
1385 !reference_type.base_type().get_bool(ID_C_constant) ||
1387 return false;
1388
1389 // TODO: handle the case for implicit parameters
1390 if(
1391 !reference_type.base_type().get_bool(ID_C_constant) &&
1392 !expr.get_bool(ID_C_lvalue))
1393 return false;
1394
1395 exprt arg_expr=expr;
1396
1397 if(arg_expr.type().id() == ID_struct_tag)
1398 {
1399 // required to initialize the temporary
1400 arg_expr.set(ID_C_lvalue, true);
1401 }
1402
1405 {
1407 tmp.add_source_location()=new_expr.source_location();
1408 new_expr.swap(tmp);
1409 return true;
1410 }
1411
1415 {
1416 {
1417 // create temporary object
1421 expr.source_location());
1422 tmp.set(ID_mode, ID_cpp);
1423 // tmp.set(ID_C_lvalue, true);
1424 tmp.add_to_operands(std::move(new_expr));
1425 new_expr.swap(tmp);
1426 }
1427
1429 tmp.type().set(ID_C_reference, true);
1430 tmp.add_source_location()=new_expr.source_location();
1431
1432 new_expr=tmp;
1433 return true;
1434 }
1435
1436 return false;
1437}
1438
1446 const exprt &expr,
1447 const typet &type,
1448 exprt &new_expr,
1449 unsigned &rank)
1450{
1451 unsigned backup_rank=rank;
1452
1453 exprt e=expr;
1455
1456 if(is_reference(type))
1457 {
1459 return false;
1460
1461 #if 0
1462 simplify_exprt simplify(*this);
1463 simplify.simplify(new_expr);
1464 new_expr.type().set(ID_C_reference, true);
1465 #endif
1466 }
1467 else if(!standard_conversion_sequence(e, type, new_expr, rank))
1468 {
1471 {
1472 if(
1473 type.id() == ID_integer &&
1474 (expr.type().id() == ID_signedbv || expr.type().id() == ID_unsignedbv))
1475 {
1476 // This is a nonstandard implicit conversion, from
1477 // bit-vectors to unbounded integers.
1478 rank = 0;
1479 new_expr = typecast_exprt(expr, type);
1480 return true;
1481 }
1482 else if(
1483 (type.id() == ID_signedbv || type.id() == ID_unsignedbv) &&
1484 expr.type().id() == ID_integer)
1485 {
1486 // This is a nonstandard implicit conversion, from
1487 // unbounded integers to bit-vectors.
1488 rank = 0;
1489 new_expr = typecast_exprt(expr, type);
1490 return true;
1491 }
1492
1493 // no conversion
1494 return false;
1495 }
1496
1497#if 0
1498 simplify_exprt simplify(*this);
1499 simplify.simplify(new_expr);
1500#endif
1501 }
1502
1503 return true;
1504}
1505
1512 const exprt &expr,
1513 const typet &type,
1514 exprt &new_expr)
1515{
1516 unsigned rank=0;
1517 return implicit_conversion_sequence(expr, type, new_expr, rank);
1518}
1519
1526 const exprt &expr,
1527 const typet &type,
1528 unsigned &rank)
1529{
1531 return implicit_conversion_sequence(expr, type, new_expr, rank);
1532}
1533
1535{
1536 exprt e=expr;
1537
1538 if(
1539 e.id() == ID_initializer_list && cpp_is_pod(type) &&
1540 e.operands().size() == 1)
1541 {
1542 e = to_unary_expr(expr).op();
1543 }
1544
1545 if(!implicit_conversion_sequence(e, type, expr))
1546 {
1549 error() << "invalid implicit conversion from '" << to_string(e.type())
1550 << "' to '" << to_string(type) << "'" << eom;
1551#if 0
1552 str << "\n " << e.type().pretty() << '\n';
1553 str << "\n " << type.pretty() << '\n';
1554#endif
1555 throw 0;
1556 }
1557}
1558
1602 exprt &expr,
1604{
1606
1607 unsigned rank=0;
1610 {
1611 expr.swap(new_expr);
1612 return;
1613 }
1614
1616 error() << "bad reference initializer" << eom;
1617 throw 0;
1618}
1619
1621 const typet &t1,
1622 const typet &t2) const
1623{
1624 PRECONDITION(t1.id() == ID_pointer && t2.id() == ID_pointer);
1625 typet nt1=t1;
1626 typet nt2=t2;
1627
1628 if(is_reference(nt1))
1629 nt1.remove(ID_C_reference);
1630 nt1.remove(ID_to_member);
1631
1632 if(is_reference(nt2))
1633 nt2.remove(ID_C_reference);
1634 nt2.remove(ID_to_member);
1635
1636 // substitute final subtypes
1637 std::vector<typet> snt1;
1638 snt1.push_back(nt1);
1639
1640 while(snt1.back().has_subtype())
1641 {
1642 snt1.reserve(snt1.size()+1);
1643 snt1.push_back(to_type_with_subtype(snt1.back()).subtype());
1644 }
1645
1647 q1.read(snt1.back());
1648
1650 q1.write(newnt1);
1651 snt1.back()=newnt1;
1652
1653 std::vector<typet> snt2;
1654 snt2.push_back(nt2);
1655 while(snt2.back().has_subtype())
1656 {
1657 snt2.reserve(snt2.size()+1);
1658 snt2.push_back(to_type_with_subtype(snt2.back()).subtype());
1659 }
1660
1662 q2.read(snt2.back());
1663
1665 q2.write(newnt2);
1666 snt2.back()=newnt2;
1667
1668 const std::size_t k=snt1.size() < snt2.size() ? snt1.size() : snt2.size();
1669
1670 for(std::size_t i=k; i > 1; i--)
1671 {
1672 to_type_with_subtype(snt1[snt1.size() - 2]).subtype() =
1673 snt1[snt1.size() - 1];
1674 snt1.pop_back();
1675
1676 to_type_with_subtype(snt2[snt2.size() - 2]).subtype() =
1677 snt2[snt2.size() - 1];
1678 snt2.pop_back();
1679 }
1680
1681 exprt e1("Dummy", snt1.back());
1682 exprt e2;
1683
1684 return !standard_conversion_qualification(e1, snt2.back(), e2);
1685}
1686
1688 const exprt &expr,
1689 const typet &type,
1690 exprt &new_expr)
1691{
1692 PRECONDITION(!is_reference(expr.type()));
1693
1694 exprt curr_expr=expr;
1695
1696 if(curr_expr.type().id()==ID_array)
1697 {
1698 if(type.id()==ID_pointer)
1699 {
1701 return false;
1702 }
1703 }
1704 else if(curr_expr.type().id()==ID_code &&
1705 type.id()==ID_pointer)
1706 {
1708 return false;
1709 }
1710 else if(curr_expr.get_bool(ID_C_lvalue))
1711 {
1713 return false;
1714 }
1715 else
1717
1718 if(is_reference(type))
1719 {
1720 if(!expr.get_bool(ID_C_lvalue))
1721 return false;
1722
1723 if(new_expr.type() != to_reference_type(type).base_type())
1724 return false;
1725
1729 return true;
1730 }
1731 else if(type.id()==ID_pointer)
1732 {
1733 if(type!=new_expr.type())
1734 return false;
1735
1736 // add proper typecast
1737 typecast_exprt typecast_expr(expr, type);
1738 new_expr.swap(typecast_expr);
1739 return true;
1740 }
1741
1742 return false;
1743}
1744
1746 const exprt &expr,
1747 const typet &type,
1748 exprt &new_expr)
1749{
1750 exprt e(expr);
1751
1752 if(type.id()==ID_pointer)
1753 {
1755 e = to_dereference_expr(expr).pointer();
1756
1757 if(e.type().id()==ID_pointer &&
1758 cast_away_constness(e.type(), type))
1759 return false;
1760 }
1761
1763
1764 if(is_reference(type))
1765 {
1766 if(to_reference_type(type).base_type().id() != ID_struct_tag)
1767 return false;
1768 }
1769 else if(type.id()==ID_pointer)
1770 {
1771 if(type.find(ID_to_member).is_not_nil())
1772 return false;
1773
1774 if(to_pointer_type(type).base_type().id() == ID_empty)
1775 {
1776 if(!e.get_bool(ID_C_lvalue))
1777 return false;
1778 UNREACHABLE; // currently not supported
1779 }
1780 else if(to_pointer_type(type).base_type().id() == ID_struct_tag)
1781 {
1782 if(e.get_bool(ID_C_lvalue))
1783 {
1784 exprt tmp(e);
1785
1787 return false;
1788 }
1789 }
1790 else return false;
1791 }
1792 else return false;
1793
1794 return static_typecast(e, type, new_expr);
1795}
1796
1798 const exprt &expr,
1799 const typet &type,
1800 exprt &new_expr,
1801 bool check_constantness)
1802{
1803 exprt e=expr;
1804
1805 if(check_constantness && type.id()==ID_pointer)
1806 {
1808 e = to_dereference_expr(expr).pointer();
1809
1810 if(e.type().id()==ID_pointer &&
1811 cast_away_constness(e.type(), type))
1812 return false;
1813 }
1814
1816
1817 if(!is_reference(type))
1818 {
1819 exprt tmp;
1820
1821 if(e.id()==ID_code)
1822 {
1824 e.swap(tmp);
1825 else
1826 return false;
1827 }
1828
1829 if(e.type().id()==ID_array)
1830 {
1832 e.swap(tmp);
1833 else
1834 return false;
1835 }
1836
1837 if(e.get_bool(ID_C_lvalue))
1838 {
1840 e.swap(tmp);
1841 else
1842 return false;
1843 }
1844 }
1845
1846 if(e.type().id()==ID_pointer &&
1847 (type.id()==ID_unsignedbv || type.id()==ID_signedbv))
1848 {
1849 // pointer to integer, always ok
1851 return true;
1852 }
1853
1854 if(
1855 (e.type().id() == ID_unsignedbv || e.type().id() == ID_signedbv ||
1856 e.type().id() == ID_c_bool || e.is_boolean()) &&
1857 type.id() == ID_pointer && !is_reference(type))
1858 {
1859 // integer to pointer
1860 if(simplify_expr(e, *this).is_zero())
1861 {
1862 // NULL
1863 new_expr=e;
1865 new_expr.type()=type;
1866 }
1867 else
1868 {
1870 }
1871 return true;
1872 }
1873
1874 if(e.type().id()==ID_pointer &&
1875 type.id()==ID_pointer &&
1876 !is_reference(type))
1877 {
1878 // pointer to pointer: we ok it all.
1879 // This is more generous than the standard.
1881 return true;
1882 }
1883
1884 if(is_reference(type) && e.get_bool(ID_C_lvalue))
1885 {
1887 return true;
1888 }
1889
1890 return false;
1891}
1892
1894 const exprt &expr, // source expression
1895 const typet &type, // destination type
1896 exprt &new_expr,
1897 bool check_constantness)
1898{
1899 exprt e=expr;
1900
1901 if(check_constantness && type.id()==ID_pointer)
1902 {
1904 e = to_dereference_expr(expr).pointer();
1905
1906 if(e.type().id()==ID_pointer &&
1907 cast_away_constness(e.type(), type))
1908 return false;
1909 }
1910
1912
1913 if(type.get_bool(ID_C_reference))
1914 {
1916 unsigned rank=0;
1918 return true;
1919
1921 typet from = e.type();
1922
1923 if(subto.id() == ID_struct_tag && from.id() == ID_struct_tag)
1924 {
1925 if(!expr.get_bool(ID_C_lvalue))
1926 return false;
1927
1929 qual_from.read(e.type());
1930
1932 qual_to.read(subto);
1933
1934 if(!qual_to.is_subset_of(qual_from))
1935 return false;
1936
1939
1941 {
1942 if(e.id()==ID_dereference)
1943 {
1945 new_expr.swap(to_dereference_expr(e).pointer());
1946 return true;
1947 }
1948
1951 new_expr.swap(address_of);
1952 return true;
1953 }
1954 }
1955 return false;
1956 }
1957
1958 if(type.id()==ID_empty)
1959 {
1961 return true;
1962 }
1963
1964 // int/enum to enum
1965 if(type.id()==ID_c_enum_tag &&
1966 (e.type().id()==ID_signedbv ||
1967 e.type().id()==ID_unsignedbv ||
1968 e.type().id()==ID_c_enum_tag))
1969 {
1971 new_expr.remove(ID_C_lvalue);
1972 return true;
1973 }
1974
1976 {
1977 if(!cpp_is_pod(type))
1978 {
1981 e.source_location(),
1982 type,
1983 already_typechecked_exprt{new_expr},
1984 temporary);
1985 new_expr.swap(temporary);
1986 }
1987 else
1988 {
1989 // try to avoid temporary
1991 if(new_expr.get_bool(ID_C_lvalue))
1992 new_expr.remove(ID_C_lvalue);
1993 }
1994
1995 return true;
1996 }
1997
1998 if(type.id()==ID_pointer && e.type().id()==ID_pointer)
1999 {
2001 if(type.find(ID_to_member).is_nil() && e.type().find(ID_to_member).is_nil())
2002 {
2004 typet from = to_pointer_type(e.type()).base_type();
2005
2006 if(from.id()==ID_empty)
2007 {
2009 return true;
2010 }
2011
2012 if(to.id() == ID_struct_tag && from.id() == ID_struct_tag)
2013 {
2014 if(e.get_bool(ID_C_lvalue))
2015 {
2016 exprt tmp(e);
2018 return false;
2019 }
2020
2024 {
2026 new_expr.swap(e);
2027 return true;
2028 }
2029 }
2030
2031 return false;
2032 }
2033 else if(
2034 type.find(ID_to_member).is_not_nil() &&
2035 e.type().find(ID_to_member).is_not_nil())
2036 {
2037 if(pointer_type.base_type() != to_pointer_type(e.type()).base_type())
2038 return false;
2039
2041 static_cast<const typet &>(e.type().find(ID_to_member))));
2042
2044 static_cast<const typet &>(type.find(ID_to_member))));
2045
2047 {
2049 return true;
2050 }
2051 }
2052 else if(
2053 type.find(ID_to_member).is_nil() &&
2054 e.type().find(ID_to_member).is_not_nil())
2055 {
2056 if(pointer_type.base_type() != to_pointer_type(e.type()).base_type())
2057 {
2058 return false;
2059 }
2060
2062 static_cast<const typet &>(e.type().find(ID_to_member)));
2063
2064 new_expr = e;
2066
2067 return true;
2068 }
2069 else
2070 return false;
2071 }
2072
2073 return false;
2074}
configt config
Definition config.cpp:25
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
floatbv_typet float_type()
Definition c_types.cpp:177
reference_typet reference_type(const typet &subtype)
Definition c_types.cpp:240
signedbv_typet signed_int_type()
Definition c_types.cpp:22
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:235
typet c_bool_type()
Definition c_types.cpp:100
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 union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition c_types.h:184
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition c_types.h:224
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
static void make_already_typechecked(exprt &expr)
The Boolean type.
Definition std_types.h:36
Base type of functions.
Definition std_types.h:583
const parameterst & parameters() const
Definition std_types.h:699
const typet & return_type() const
Definition std_types.h:689
struct configt::ansi_ct ansi_c
bool reference_compatible(const exprt &expr, const reference_typet &type, unsigned &rank) const
Reference-compatible.
bool implicit_conversion_sequence(const exprt &expr, const typet &type, exprt &new_expr, unsigned &rank)
implicit conversion sequence
bool standard_conversion_floating_point_conversion(const exprt &expr, const typet &type, exprt &new_expr) const
Floating-point conversion.
bool reinterpret_typecast(const exprt &expr, const typet &type, exprt &new_expr, bool check_constantness=true)
bool standard_conversion_boolean(const exprt &expr, exprt &new_expr) const
Boolean conversion.
bool standard_conversion_pointer(const exprt &expr, const typet &type, exprt &new_expr)
Pointer conversion.
void implicit_typecast(exprt &expr, const typet &type) override
bool reference_related(const exprt &expr, const reference_typet &type) const
Reference-related.
bool standard_conversion_integral_conversion(const exprt &expr, const typet &type, exprt &new_expr) const
Integral conversion.
bool standard_conversion_sequence(const exprt &expr, const typet &type, exprt &new_expr, unsigned &rank)
Standard Conversion Sequence.
bool standard_conversion_qualification(const exprt &expr, const typet &, exprt &new_expr) const
Qualification conversion.
void typecheck_side_effect_function_call(side_effect_expr_function_callt &) override
bool cpp_is_pod(const typet &type) const
bool standard_conversion_floating_point_promotion(const exprt &expr, exprt &new_expr) const
Floating-point-promotion conversion.
bool standard_conversion_floating_integral_conversion(const exprt &expr, const typet &type, exprt &new_expr) const
Floating-integral conversion.
bool const_typecast(const exprt &expr, const typet &type, exprt &new_expr)
void new_temporary(const source_locationt &source_location, const typet &, const exprt::operandst &ops, exprt &temporary)
void show_instantiation_stack(std::ostream &)
bool standard_conversion_function_to_pointer(const exprt &expr, exprt &new_expr) const
Function-to-pointer conversion.
bool standard_conversion_array_to_pointer(const exprt &expr, exprt &new_expr) const
Array-to-pointer conversion.
bool dynamic_typecast(const exprt &expr, const typet &type, exprt &new_expr)
bool user_defined_conversion_sequence(const exprt &expr, const typet &type, exprt &new_expr, unsigned &rank)
User-defined conversion sequence.
bool standard_conversion_lvalue_to_rvalue(const exprt &expr, exprt &new_expr) const
Lvalue-to-rvalue conversion.
bool cast_away_constness(const typet &t1, const typet &t2) const
void add_implicit_dereference(exprt &)
bool static_typecast(const exprt &expr, const typet &type, exprt &new_expr, bool check_constantness=true)
bool subtype_typecast(const struct_typet &from, const struct_typet &to) const
void make_ptr_typecast(exprt &expr, const pointer_typet &dest_type)
bool standard_conversion_integral_promotion(const exprt &expr, exprt &new_expr) const
Integral-promotion conversion.
std::string to_string(const typet &) override
bool standard_conversion_pointer_to_member(const exprt &expr, const typet &type, exprt &new_expr)
Pointer-to-member conversion.
void reference_initializer(exprt &expr, const reference_typet &type)
A reference to type "cv1 T1" is initialized by an expression of type "cv2 T2" as follows:
bool reference_binding(exprt expr, const reference_typet &type, exprt &new_expr, unsigned &rank)
Reference binding.
Operator to dereference a pointer.
Base class for all expressions.
Definition expr.h:56
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition expr.cpp:147
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition expr.h:224
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:212
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
const source_locationt & source_location() const
Definition expr.h:231
Array index operator.
Definition std_expr.h:1470
bool get_bool(const irep_idt &name) const
Definition irep.cpp:57
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition irep.cpp:482
const irept & find(const irep_idt &name) const
Definition irep.cpp:93
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
void remove(const irep_idt &name)
Definition irep.cpp:87
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:412
void swap(irept &irep)
Definition irep.h:434
const irep_idt & id() const
Definition irep.h:388
source_locationt source_location
Definition message.h:239
mstreamt & error() const
Definition message.h:391
static eomt eom
Definition message.h:289
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition namespace.cpp:49
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
const typet & base_type() const
The type of the data what we point to.
The reference type.
A side_effect_exprt representation of a function call side effect.
Definition std_code.h:1692
An expression containing a side effect.
Definition std_code.h:1450
A struct tag type, i.e., struct_typet with an identifier.
Definition std_types.h:493
Structure type, corresponds to C style structs.
Definition std_types.h:231
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
C++ Language Type Checking.
symbol_exprt cpp_symbol_expr(const symbolt &symbol)
Definition cpp_util.cpp:14
exprt is_not_zero(const exprt &src, const namespacet &ns)
converts a scalar/float expression to C/C++ Booleans
Definition expr_util.cpp:74
bool is_null_pointer(const constant_exprt &expr)
Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...
Deprecated expression utility functions.
API to expression classes for Pointers.
bool is_reference(const typet &type)
Returns true if the type is a reference.
const reference_typet & to_reference_type(const typet &type)
Cast a typet to a reference_typet.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
bool simplify(exprt &expr, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition std_expr.cpp:97
API to expression classes.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:426
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition std_expr.h:987
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:3172
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:788
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition std_types.h:308
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition std_types.h:518
const tag_typet & to_tag_type(const typet &type)
Cast a typet to a tag_typet.
Definition std_types.h:434
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition type.h:208