Skip to content

Remove unused parameter from float_bvt::is_zero #2433

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Jun 24, 2018
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 7 additions & 9 deletions src/solvers/floatbv/float_bv.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -64,7 +64,7 @@ exprt float_bvt::convert(const exprt &expr)
else if(expr.id()==ID_typecast &&
expr.type().id()==ID_bool &&
expr.op0().type().id()==ID_floatbv) // float -> bool
return not_exprt(is_zero(expr.op0(), get_spec(expr.op0())));
return not_exprt(is_zero(expr.op0()));
else if(expr.id()==ID_floatbv_plus)
return add_sub(false, expr.op0(), expr.op1(), expr.op2(), get_spec(expr));
else if(expr.id()==ID_floatbv_minus)
Expand Down Expand Up @@ -129,8 +129,8 @@ exprt float_bvt::is_equal(
const ieee_float_spect &spec)
{
// special cases: -0 and 0 are equal
exprt is_zero0=is_zero(src0, spec);
exprt is_zero1=is_zero(src1, spec);
const exprt is_zero0 = is_zero(src0);
const exprt is_zero1 = is_zero(src1);
const and_exprt both_zero(is_zero0, is_zero1);

// NaN compares to nothing
Expand All @@ -145,9 +145,7 @@ exprt float_bvt::is_equal(
not_exprt(nan));
}

exprt float_bvt::is_zero(
const exprt &src,
const ieee_float_spect &spec)
exprt float_bvt::is_zero(const exprt &src)
{
// we mask away the sign bit, which is the most significant bit
const floatbv_typet &type=to_floatbv_type(src.type());
Expand Down Expand Up @@ -743,8 +741,8 @@ exprt float_bvt::relation(
assert(rel==relt::EQ || rel==relt::LT || rel==relt::LE);

// special cases: -0 and 0 are equal
exprt is_zero1=is_zero(src1, spec);
exprt is_zero2=is_zero(src2, spec);
const exprt is_zero1 = is_zero(src1);
const exprt is_zero2 = is_zero(src2);
const and_exprt both_zero(is_zero1, is_zero2);

// NaN compares to nothing
Expand Down Expand Up @@ -1346,7 +1344,7 @@ float_bvt::unbiased_floatt float_bvt::unpack(
sub_bias(result.exponent, spec));

result.infinity=isinf(src, spec);
result.zero=is_zero(src, spec);
result.zero = is_zero(src);
result.NaN=isnan(src, spec);

return result;
Expand Down
2 changes: 1 addition & 1 deletion src/solvers/floatbv/float_bv.h
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,7 @@ class float_bvt
exprt negation(const exprt &, const ieee_float_spect &);
exprt abs(const exprt &, const ieee_float_spect &);
exprt is_equal(const exprt &, const exprt &, const ieee_float_spect &);
exprt is_zero(const exprt &, const ieee_float_spect &);
exprt is_zero(const exprt &);
exprt isnan(const exprt &, const ieee_float_spect &);
exprt isinf(const exprt &, const ieee_float_spect &);
exprt isnormal(const exprt &, const ieee_float_spect &);
Expand Down