Skip to content

Use appropriate numeric_cast_v<T> instead of deprecated integer2unsigned #3047

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
Oct 15, 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
5 changes: 1 addition & 4 deletions src/ansi-c/expr2c.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -2219,10 +2219,7 @@ std::string expr2ct::convert_array(
if(it==--src.operands().end())
break;

assert(it->is_constant());
mp_integer i;
to_integer(*it, i);
unsigned int ch=integer2unsigned(i);
const unsigned int ch = numeric_cast_v<unsigned>(*it);

if(last_was_hex)
{
Expand Down
2 changes: 1 addition & 1 deletion src/solvers/flattening/boolbv_byte_update.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -60,7 +60,7 @@ bvt boolbvt::convert_byte_update(const byte_update_exprt &expr)
bv_endianness_mapt map_op(op.type(), false, ns, boolbv_width);
bv_endianness_mapt map_value(value.type(), false, ns, boolbv_width);

std::size_t offset_i=integer2unsigned(offset);
const std::size_t offset_i = numeric_cast_v<std::size_t>(offset);

for(std::size_t i=0; i<update_width; i++)
{
Expand Down
2 changes: 1 addition & 1 deletion src/solvers/flattening/boolbv_extractbits.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -54,7 +54,7 @@ bvt boolbvt::convert_extractbits(const extractbits_exprt &expr)
expr.find_source_location(),
irep_pretty_diagnosticst{expr});

const std::size_t offset = integer2unsigned(lower_as_int);
const std::size_t offset = numeric_cast_v<std::size_t>(lower_as_int);

bvt result_bv(src_bv.begin() + offset, src_bv.begin() + offset + bv_width);

Expand Down
2 changes: 1 addition & 1 deletion src/solvers/flattening/boolbv_replication.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@ bvt boolbvt::convert_replication(const replication_exprt &expr)
bvt bv;
bv.resize(width);

const std::size_t u_times=integer2unsigned(times);
const std::size_t u_times = numeric_cast_v<std::size_t>(times);
const bvt &op = convert_bv(expr.op());

INVARIANT(
Expand Down
8 changes: 4 additions & 4 deletions src/solvers/flattening/boolbv_width.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -141,7 +141,7 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
if(total>(1<<30)) // realistic limit
throw analysis_exceptiont("array too large for flattening");

entry.total_width=integer2unsigned(total);
entry.total_width = numeric_cast_v<std::size_t>(total);
}
}
else if(type_id==ID_vector)
Expand All @@ -162,13 +162,13 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
if(total>(1<<30)) // realistic limit
analysis_exceptiont("vector too large for flattening");

entry.total_width=integer2unsigned(vector_size*sub_width);
entry.total_width = numeric_cast_v<std::size_t>(vector_size * sub_width);
}
}
else if(type_id==ID_complex)
{
std::size_t sub_width=operator()(type.subtype());
entry.total_width=integer2unsigned(2*sub_width);
const mp_integer sub_width = operator()(type.subtype());
entry.total_width = numeric_cast_v<std::size_t>(2 * sub_width);
}
else if(type_id==ID_code)
{
Expand Down
5 changes: 3 additions & 2 deletions src/solvers/flattening/boolbv_with.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -152,7 +152,8 @@ void boolbvt::convert_with_array(

if(op1_value>=0 && op1_value<size) // bounds check
{
std::size_t offset=integer2unsigned(op1_value*op2_bv.size());
const std::size_t offset =
numeric_cast_v<std::size_t>(op1_value * op2_bv.size());

for(std::size_t j=0; j<op2_bv.size(); j++)
next_bv[offset+j]=op2_bv[j];
Expand All @@ -169,7 +170,7 @@ void boolbvt::convert_with_array(

literalt eq_lit=convert(equal_exprt(op1, counter));

std::size_t offset=integer2unsigned(i*op2_bv.size());
const std::size_t offset = numeric_cast_v<std::size_t>(i * op2_bv.size());

for(std::size_t j=0; j<op2_bv.size(); j++)
next_bv[offset+j]=
Expand Down
8 changes: 5 additions & 3 deletions src/solvers/flattening/flatten_byte_operators.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -330,7 +330,7 @@ exprt flatten_byte_extract(
const typet &offset_type=ns.follow(offset.type());

// get 'width'-many bytes, and concatenate
std::size_t width_bytes=integer2unsigned(num_elements);
const std::size_t width_bytes = numeric_cast_v<std::size_t>(num_elements);
exprt::operandst op;
op.reserve(width_bytes);

Expand Down Expand Up @@ -567,10 +567,12 @@ exprt flatten_byte_update(
// zero-extend the value, but only if needed
exprt value_extended;

if(width>integer2unsigned(element_size)*8)
if(width > element_size * 8)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This looks inconsistent: width is a size_t (which is parsed with integer2size_t above). element_size is an mp_integer.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thus everything will be converted to mp_integer, which avoids falling for an (unsigned) integer overflow.

value_extended = concatenation_exprt(
from_integer(
0, unsignedbv_typet(width - integer2unsigned(element_size) * 8)),
0,
unsignedbv_typet(
width - numeric_cast_v<std::size_t>(element_size) * 8)),
src.value(),
t);
else
Expand Down
5 changes: 3 additions & 2 deletions src/solvers/qbf/qbf_qube_core.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ Author: CM Wintersteiger
#include <cstring>
#include <fstream>

#include <util/arith_tools.h>
#include <util/invariant.h>
#include <util/mp_arith.h>

Expand Down Expand Up @@ -78,9 +79,9 @@ propt::resultt qbf_qube_coret::prop_solve()
{
mp_integer b(line.substr(2).c_str());
if(b<0)
assignment[integer2unsigned(b.negate())]=false;
assignment[numeric_cast_v<std::size_t>(b.negate())] = false;
else
assignment[integer2unsigned(b)]=true;
assignment[numeric_cast_v<std::size_t>(b)] = true;
}
else if(line=="s cnf 1")
{
Expand Down
2 changes: 1 addition & 1 deletion src/util/arith_tools.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -100,7 +100,7 @@ bool to_unsigned_integer(const constant_exprt &expr, unsigned &uint_value)
return true;
else
{
uint_value=integer2unsigned(i);
uint_value = numeric_cast_v<unsigned>(i);
return false;
}
}
Expand Down
2 changes: 1 addition & 1 deletion src/util/config.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -1136,7 +1136,7 @@ static unsigned unsigned_from_ns(
"symbol table configuration entry `" + id2string(id) +
"' must be convertible to mp_integer");

return integer2unsigned(int_value);
return numeric_cast_v<unsigned>(int_value);
}

void configt::set_from_symbol_table(
Expand Down