File tree 1 file changed +4
-8
lines changed
1 file changed +4
-8
lines changed Original file line number Diff line number Diff line change @@ -1057,13 +1057,9 @@ void value_sett::get_reference_set_rec(
1057
1057
insert (dest, exprt (ID_unknown, expr.type ()));
1058
1058
else
1059
1059
{
1060
- index_exprt index_expr (expr.type ());
1061
- index_expr.array ()=object;
1062
- index_expr.index ()=from_integer (0 , index_type ());
1063
-
1064
- // adjust type?
1065
- if (ns.follow (object.type ())!=array_type)
1066
- index_expr.make_typecast (array.type ());
1060
+ const index_exprt deref_index_expr (
1061
+ typecast_exprt::conditional_cast (object, array_type),
1062
+ from_integer (0 , index_type ()));
1067
1063
1068
1064
offsett o = a_it->second ;
1069
1065
mp_integer i;
@@ -1083,7 +1079,7 @@ void value_sett::get_reference_set_rec(
1083
1079
else
1084
1080
o.reset ();
1085
1081
1086
- insert (dest, index_expr , o);
1082
+ insert (dest, deref_index_expr , o);
1087
1083
}
1088
1084
}
1089
1085
You can’t perform that action at this time.
0 commit comments