Skip to content

Commit 39d38f1

Browse files
author
Daniel Kroening
committed
replace exprt::make_typecast() by typecast_exprt()
exprt::make_typecast() isn't type safe
1 parent 6c14669 commit 39d38f1

File tree

3 files changed

+19
-7
lines changed

3 files changed

+19
-7
lines changed

src/pointer-analysis/value_set_fi.cpp

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -853,9 +853,13 @@ void value_set_fit::get_reference_set_sharing_rec(
853853
index_exprt index_expr(
854854
object, from_integer(0, index_type()), expr.type());
855855

856+
exprt casted_index;
857+
856858
// adjust type?
857859
if(object.type().id() != "#REF#" && object.type() != array_type)
858-
index_expr.make_typecast(array.type());
860+
casted_index = typecast_exprt(index_expr, array.type());
861+
else
862+
casted_index = index_expr;
859863

860864
offsett o = a_it->second;
861865
mp_integer i;
@@ -868,7 +872,7 @@ void value_set_fit::get_reference_set_sharing_rec(
868872
else
869873
o.reset();
870874

871-
insert(dest, index_expr, o);
875+
insert(dest, casted_index, o);
872876
}
873877
}
874878

src/pointer-analysis/value_set_fivr.cpp

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -964,9 +964,13 @@ void value_set_fivrt::get_reference_set_sharing_rec(
964964
index_exprt index_expr(
965965
object, from_integer(0, index_type()), expr.type());
966966

967+
exprt casted_index;
968+
967969
// adjust type?
968970
if(object.type().id() != "#REF#" && object.type() != array_type)
969-
index_expr.make_typecast(array.type());
971+
casted_index = typecast_exprt(index_expr, array.type());
972+
else
973+
casted_index = index_expr;
970974

971975
offsett o = a_it->second;
972976
mp_integer i;
@@ -979,7 +983,7 @@ void value_set_fivrt::get_reference_set_sharing_rec(
979983
else
980984
o.reset();
981985

982-
insert_from(dest, index_expr, o);
986+
insert_from(dest, casted_index, o);
983987
}
984988
}
985989

src/pointer-analysis/value_set_fivrns.cpp

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -657,9 +657,13 @@ void value_set_fivrnst::get_reference_set_rec(
657657
index_exprt index_expr(
658658
object, from_integer(0, index_type()), expr.type());
659659

660+
exprt casted_index;
661+
660662
// adjust type?
661-
if(object.type() != array_type)
662-
index_expr.make_typecast(array.type());
663+
if(object.type().id() != "#REF#" && object.type() != array_type)
664+
casted_index = typecast_exprt(index_expr, array.type());
665+
else
666+
casted_index = index_expr;
663667

664668
offsett o = a_it->second;
665669
mp_integer i;
@@ -672,7 +676,7 @@ void value_set_fivrnst::get_reference_set_rec(
672676
else
673677
o.reset();
674678

675-
insert_from(dest, index_expr, o);
679+
insert_from(dest, casted_index, o);
676680
}
677681
}
678682

0 commit comments

Comments
 (0)