Merge pull request #3047 from tautschnig/integer2unsigned

Use appropriate numeric_cast_v<T> instead of deprecated integer2unsigned
This commit is contained in:
Daniel Kroening 2018-10-15 08:48:39 +01:00 committed by GitHub
commit 7bf48c0cb0
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
10 changed files with 21 additions and 20 deletions

View File

@ -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)
{

View File

@ -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++)
{

View File

@ -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);

View File

@ -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(

View File

@ -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)
@ -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)
{

View File

@ -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];
@ -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]=

View File

@ -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);
@ -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)
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

View File

@ -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>
@ -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")
{

View File

@ -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;
}
}

View File

@ -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(