Skip to content

Remove set but not used variables #8595

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.

Sign up for GitHub

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
Apr 4, 2025
Merged

Remove set but not used variables #8595

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
8 changes: 3 additions & 5 deletions src/solvers/flattening/boolbv_overflow.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -125,15 +125,14 @@
? bv_utilst::representationt::SIGNED
: bv_utilst::representationt::UNSIGNED;

if(
const auto plus_overflow = expr_try_dynamic_cast<plus_overflow_exprt>(expr))
if(expr_try_dynamic_cast<plus_overflow_exprt>(expr))
{
if(bv0.size() != bv1.size())
return SUB::convert_rest(expr);

return bv_utils.overflow_add(bv0, bv1, rep);
}
if(const auto minus = expr_try_dynamic_cast<minus_overflow_exprt>(expr))
if(expr_try_dynamic_cast<minus_overflow_exprt>(expr))
{
if(bv0.size() != bv1.size())
return SUB::convert_rest(expr);
Expand All @@ -158,8 +157,7 @@

return mult_overflow_result(prop, bv0, bv1, rep).back();
}
else if(
const auto shl_overflow = expr_try_dynamic_cast<shl_overflow_exprt>(expr))
else if(expr_try_dynamic_cast<shl_overflow_exprt>(expr))

Check warning on line 160 in src/solvers/flattening/boolbv_overflow.cpp

View check run for this annotation

Codecov / codecov/patch

src/solvers/flattening/boolbv_overflow.cpp#L160 

Added line #L160 was not covered by tests
{
DATA_INVARIANT(!bv0.empty(), "zero-sized operand");

Expand Down
10 changes: 4 additions & 6 deletions src/solvers/smt2_incremental/convert_expr_to_smt.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -175,14 +175,14 @@ static smt_termt make_bitvector_resize_cast(
const bitvector_typet &from_type,
const bitvector_typet &to_type)
{
if(const auto to_fixedbv_type = type_try_dynamic_cast<fixedbv_typet>(to_type))
if(type_try_dynamic_cast<fixedbv_typet>(to_type))
{
UNIMPLEMENTED_FEATURE(
"Generation of SMT formula for type cast to fixed-point bitvector "
"type: " +
to_type.pretty());
}
if(const auto to_floatbv_type = type_try_dynamic_cast<floatbv_typet>(to_type))
if(type_try_dynamic_cast<floatbv_typet>(to_type))
{
UNIMPLEMENTED_FEATURE(
"Generation of SMT formula for type cast to floating-point bitvector "
Expand Down Expand Up @@ -258,7 +258,7 @@ static smt_termt convert_expr_to_smt(
const auto &from_term = converted.at(cast.op());
const typet &from_type = cast.op().type();
const typet &to_type = cast.type();
if(const auto bool_type = type_try_dynamic_cast<bool_typet>(to_type))
if(type_try_dynamic_cast<bool_typet>(to_type))
return make_not_zero(from_term, cast.op().type());
if(const auto c_bool_type = type_try_dynamic_cast<c_bool_typet>(to_type))
return convert_c_bool_cast(from_term, from_type, *c_bool_type);
Expand Down Expand Up @@ -893,9 +893,7 @@ static smt_termt convert_expr_to_smt(
"Pointer should be wider than object_bits in order to allow for offset "
"encoding.");
const size_t offset_bits = type->get_width() - object_bits;
if(
const auto symbol =
expr_try_dynamic_cast<symbol_exprt>(address_of.object()))
if(expr_try_dynamic_cast<symbol_exprt>(address_of.object()))
{
const smt_bit_vector_constant_termt offset{0, offset_bits};
return smt_bit_vector_theoryt::concat(object_bit_vector, offset);
Expand Down
Loading