Skip to content

Commit 5f7eedc

Browse files
committed
ID_rem is not used
The C front-end generates ID_floatbv_mod and ID_floatbv_rem; ID_rem is never generated.
1 parent c0dd77e commit 5f7eedc

File tree

1 file changed

+6
-7
lines changed

1 file changed

+6
-7
lines changed

src/goto-programs/adjust_float_expressions.cpp

Lines changed: 6 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -41,9 +41,9 @@ static bool have_to_adjust_float_expressions(const exprt &expr)
4141
type.id() == ID_floatbv ||
4242
(type.id() == ID_complex && type.subtype().id() == ID_floatbv))
4343
{
44-
if(expr.id()==ID_plus || expr.id()==ID_minus ||
45-
expr.id()==ID_mult || expr.id()==ID_div ||
46-
expr.id()==ID_rem)
44+
if(
45+
expr.id() == ID_plus || expr.id() == ID_minus || expr.id() == ID_mult ||
46+
expr.id() == ID_div)
4747
return true;
4848
}
4949

@@ -95,9 +95,9 @@ void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
9595
type.id() == ID_floatbv ||
9696
(type.id() == ID_complex && type.subtype().id() == ID_floatbv))
9797
{
98-
if(expr.id()==ID_plus || expr.id()==ID_minus ||
99-
expr.id()==ID_mult || expr.id()==ID_div ||
100-
expr.id()==ID_rem)
98+
if(
99+
expr.id() == ID_plus || expr.id() == ID_minus || expr.id() == ID_mult ||
100+
expr.id() == ID_div)
101101
{
102102
DATA_INVARIANT(
103103
expr.operands().size() >= 2,
@@ -115,7 +115,6 @@ void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
115115
expr.id()==ID_minus?ID_floatbv_minus:
116116
expr.id()==ID_mult?ID_floatbv_mult:
117117
expr.id()==ID_div?ID_floatbv_div:
118-
expr.id()==ID_rem?ID_floatbv_rem:
119118
irep_idt());
120119

121120
expr.operands().resize(3);

0 commit comments

Comments
 (0)