Skip to content

Commit 19eb8c1

Browse files
author
Daniel Kroening
committed
better typing in the simplifier
1 parent 33c00c1 commit 19eb8c1

File tree

1 file changed

+10
-11
lines changed

1 file changed

+10
-11
lines changed

src/util/simplify_expr.cpp

Lines changed: 10 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -661,8 +661,7 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
661661
op_type.id() == ID_pointer && expr.op().id() == ID_plus &&
662662
expr.op().operands().size() == 2 &&
663663
((expr.op().op0().id() == ID_typecast &&
664-
expr.op().op0().operands().size() == 1 &&
665-
expr.op().op0().op0().is_zero()) ||
664+
to_typecast_expr(expr.op().op0()).op().is_zero()) ||
666665
(expr.op().op0().is_constant() &&
667666
to_constant_expr(expr.op().op0()).get_value() == ID_NULL)))
668667
{
@@ -1076,14 +1075,14 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
10761075
{
10771076
// (T1)(T2)x ---> (T1)
10781077
// where T1 has fewer bits than T2
1079-
if(operand.operands().size()==1 &&
1080-
op_type_id==expr_type_id &&
1081-
(expr_type_id==ID_unsignedbv || expr_type_id==ID_signedbv) &&
1082-
to_bitvector_type(expr_type).get_width()<=
1083-
to_bitvector_type(operand.type()).get_width())
1078+
if(
1079+
op_type_id == expr_type_id &&
1080+
(expr_type_id == ID_unsignedbv || expr_type_id == ID_signedbv) &&
1081+
to_bitvector_type(expr_type).get_width() <=
1082+
to_bitvector_type(operand.type()).get_width())
10841083
{
10851084
auto new_expr = expr;
1086-
new_expr.op() = expr.op().op0();
1085+
new_expr.op() = to_typecast_expr(operand).op();
10871086
// might enable further simplification
10881087
return changed(simplify_typecast(new_expr)); // recursive call
10891088
}
@@ -1139,9 +1138,9 @@ simplify_exprt::simplify_dereference(const dereference_exprt &expr)
11391138
return changed(simplify_rec(tmp));
11401139
}
11411140
// rewrite *(&a[0] + x) to a[x]
1142-
else if(pointer.id()==ID_plus &&
1143-
pointer.operands().size()==2 &&
1144-
pointer.op0().id()==ID_address_of)
1141+
else if(
1142+
pointer.id() == ID_plus && pointer.operands().size() == 2 &&
1143+
to_plus_expr(pointer).op0().id() == ID_address_of)
11451144
{
11461145
const address_of_exprt &address_of=
11471146
to_address_of_expr(pointer.op0());

0 commit comments

Comments
 (0)