Use numeric_cast<mp_integer> instead of deprecated to_integer(exprt), part 2

This further reduces the number of warnings flagged, in particular in
Visual-Studio builds. Also turn tests of the size of ID_vector types being
constants into invariants as was already done in some places.
This commit is contained in:
Michael Tautschnig 2018-11-03 11:26:48 +00:00
parent c2380e8f6e
commit b541bf94a9
23 changed files with 87 additions and 161 deletions

View File

@ -191,21 +191,17 @@ std::string expr2javat::convert_constant(
std::string dest;
dest.reserve(char_representation_length);
mp_integer int_value;
if(to_integer(src, int_value))
UNREACHABLE;
const char16_t int_value = numeric_cast_v<char16_t>(src);
// Character literals in Java have type 'char', thus no cast is needed.
// This is different from C, where charater literals have type 'int'.
dest += '\'' + utf16_native_endian_to_java(int_value.to_long()) + '\'';
dest += '\'' + utf16_native_endian_to_java(int_value) + '\'';
return dest;
}
else if(src.type()==java_byte_type())
{
// No byte-literals in Java, so just cast:
mp_integer int_value;
if(to_integer(src, int_value))
UNREACHABLE;
const mp_integer int_value = numeric_cast_v<mp_integer>(src);
std::string dest="(byte)";
dest+=integer2string(int_value);
return dest;
@ -213,9 +209,7 @@ std::string expr2javat::convert_constant(
else if(src.type()==java_short_type())
{
// No short-literals in Java, so just cast:
mp_integer int_value;
if(to_integer(src, int_value))
UNREACHABLE;
const mp_integer int_value = numeric_cast_v<mp_integer>(src);
std::string dest="(short)";
dest+=integer2string(int_value);
return dest;
@ -223,9 +217,7 @@ std::string expr2javat::convert_constant(
else if(src.type()==java_long_type())
{
// long integer literals must have 'L' at the end
mp_integer int_value;
if(to_integer(src, int_value))
UNREACHABLE;
const mp_integer int_value = numeric_cast_v<mp_integer>(src);
std::string dest=integer2string(int_value);
dest+='L';
return dest;

View File

@ -210,12 +210,8 @@ const exprt java_bytecode_convert_methodt::variable(
size_t address,
java_bytecode_convert_methodt::variable_cast_argumentt do_cast)
{
mp_integer number;
bool ret=to_integer(to_constant_expr(arg), number);
CHECK_RETURN(!ret);
std::size_t number_int=integer2size_t(number);
typet t=java_type_from_char(type_char);
const std::size_t number_int = numeric_cast_v<std::size_t>(arg);
variablest &var_list=variables[number_int];
// search variable in list for correct frame / address if necessary
@ -1332,9 +1328,7 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
else if(statement=="goto" || statement=="goto_w")
{
PRECONDITION(op.empty() && results.empty());
mp_integer number;
bool ret=to_integer(to_constant_expr(arg0), number);
INVARIANT(!ret, "goto argument should be an integer");
const mp_integer number = numeric_cast_v<mp_integer>(arg0);
code_gotot code_goto(label(integer2string(number)));
c=code_goto;
}
@ -1342,9 +1336,7 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
{
// As 'goto', except we must also push the subroutine return address:
PRECONDITION(op.empty() && results.size() == 1);
mp_integer number;
bool ret=to_integer(to_constant_expr(arg0), number);
INVARIANT(!ret, "jsr argument should be an integer");
const mp_integer number = numeric_cast_v<mp_integer>(arg0);
code_gotot code_goto(label(integer2string(number)));
c=code_goto;
results[0]=
@ -1386,9 +1378,7 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
else if(statement==patternt("if_?cmp??"))
{
PRECONDITION(op.size() == 2 && results.empty());
mp_integer number;
bool ret=to_integer(to_constant_expr(arg0), number);
INVARIANT(!ret, "if_?cmp?? argument should be an integer");
const mp_integer number = numeric_cast_v<mp_integer>(arg0);
c = convert_if_cmp(
address_map, statement, op, number, i_it->source_location);
}
@ -1405,25 +1395,19 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
INVARIANT(!id.empty(), "unexpected bytecode-if");
PRECONDITION(op.size() == 1 && results.empty());
mp_integer number;
bool ret=to_integer(to_constant_expr(arg0), number);
INVARIANT(!ret, "if?? argument should be an integer");
const mp_integer number = numeric_cast_v<mp_integer>(arg0);
c = convert_if(address_map, op, id, number, i_it->source_location);
}
else if(statement==patternt("ifnonnull"))
{
PRECONDITION(op.size() == 1 && results.empty());
mp_integer number;
bool ret=to_integer(to_constant_expr(arg0), number);
INVARIANT(!ret, "ifnonnull argument should be an integer");
const mp_integer number = numeric_cast_v<mp_integer>(arg0);
c = convert_ifnonull(address_map, op, number, i_it->source_location);
}
else if(statement==patternt("ifnull"))
{
PRECONDITION(op.size() == 1 && results.empty());
mp_integer number;
bool ret=to_integer(to_constant_expr(arg0), number);
INVARIANT(!ret, "ifnull argument should be an integer");
const mp_integer number = numeric_cast_v<mp_integer>(arg0);
c = convert_ifnull(address_map, op, number, i_it->source_location);
}
else if(statement=="iinc")
@ -1620,10 +1604,7 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
{
// The first argument is the type, the second argument is the number of
// dimensions. The size of each dimension is on the stack.
mp_integer number;
bool ret=to_integer(to_constant_expr(arg1), number);
INVARIANT(!ret, "multianewarray argument should be an integer");
std::size_t dimension=integer2size_t(number);
const std::size_t dimension = numeric_cast_v<std::size_t>(arg1);
op=pop(dimension);
assert(results.size()==1);
@ -1954,9 +1935,7 @@ code_switcht java_bytecode_convert_methodt::convert_switch(
code_switch_caset code_case;
code_case.add_source_location() = location;
mp_integer number;
bool ret = to_integer(to_constant_expr(*a_it), number);
DATA_INVARIANT(!ret, "case label expected to be integer");
const mp_integer number = numeric_cast_v<mp_integer>(*a_it);
// The switch case does not contain any code, it just branches via a GOTO
// to the jump target of the tableswitch/lookupswitch case at
// hand. Therefore we consider this code to belong to the source bytecode
@ -2074,9 +2053,7 @@ exprt::operandst &java_bytecode_convert_methodt::convert_const(
ieee_floatt value(spec);
if(arg0.type().id() != ID_floatbv)
{
mp_integer number;
bool ret = to_integer(to_constant_expr(arg0), number);
DATA_INVARIANT(!ret, "failed to convert constant");
const mp_integer number = numeric_cast_v<mp_integer>(arg0);
value.from_integer(number);
}
else
@ -2086,9 +2063,7 @@ exprt::operandst &java_bytecode_convert_methodt::convert_const(
}
else
{
mp_integer value;
bool ret = to_integer(to_constant_expr(arg0), value);
DATA_INVARIANT(!ret, "failed to convert constant");
const mp_integer value = numeric_cast_v<mp_integer>(arg0);
const typet type = java_type_from_char(statement[0]);
results[0] = from_integer(value, type);
}

View File

@ -90,9 +90,7 @@ refined_string_exprt make_refined_string_exprt(const array_string_exprt &arr)
/// \return the corresponding index set
std::set<exprt> full_index_set(const array_string_exprt &s)
{
PRECONDITION(s.length().is_constant());
mp_integer n;
to_integer(s.length(), n);
const mp_integer n = numeric_cast_v<mp_integer>(s.length());
std::set<exprt> ret;
for(mp_integer i=0; i<n; ++i)
ret.insert(from_integer(i));

View File

@ -1110,13 +1110,9 @@ void goto_checkt::bounds_check(
}
else
{
mp_integer i;
const auto i = numeric_cast<mp_integer>(index);
if(!to_integer(index, i) && i>=0)
{
// ok
}
else
if(!i.has_value() || *i < 0)
{
exprt effective_offset=ode.offset();

View File

@ -181,18 +181,15 @@ void rw_range_sett::get_objects_shift(
range_spect src_size = op_bits.has_value() ? to_range_spect(*op_bits) : -1;
mp_integer dist;
if(range_start==-1 ||
size==-1 ||
src_size==-1 ||
to_integer(simp_distance, dist))
const auto dist = numeric_cast<mp_integer>(simp_distance);
if(range_start == -1 || size == -1 || src_size == -1 || !dist.has_value())
{
get_objects_rec(mode, shift.op(), -1, -1);
get_objects_rec(mode, shift.distance(), -1, -1);
}
else
{
range_spect dist_r=to_range_spect(dist);
const range_spect dist_r = to_range_spect(*dist);
// not sure whether to worry about
// config.ansi_c.endianness==configt::ansi_ct::IS_LITTLE_ENDIAN
@ -284,22 +281,17 @@ void rw_range_sett::get_objects_index(
const exprt simp_index=simplify_expr(expr.index(), ns);
mp_integer index;
if(to_integer(simp_index, index))
{
const auto index = numeric_cast<mp_integer>(simp_index);
if(!index.has_value())
get_objects_rec(get_modet::READ, expr.index());
index=-1;
}
if(range_start==-1 ||
sub_size==-1 ||
index==-1)
if(range_start == -1 || sub_size == -1 || !index.has_value())
get_objects_rec(mode, expr.array(), -1, size);
else
get_objects_rec(
mode,
expr.array(),
range_start+to_range_spect(index*sub_size),
range_start + to_range_spect(*index * sub_size),
size);
}

View File

@ -254,8 +254,7 @@ void interval_domaint::assume_rec(
if(is_int(lhs.type()) && is_int(rhs.type()))
{
mp_integer tmp;
to_integer(rhs, tmp);
mp_integer tmp = numeric_cast_v<mp_integer>(rhs);
if(id==ID_lt)
--tmp;
integer_intervalt &ii=int_map[lhs_identifier];
@ -280,8 +279,7 @@ void interval_domaint::assume_rec(
if(is_int(lhs.type()) && is_int(rhs.type()))
{
mp_integer tmp;
to_integer(lhs, tmp);
mp_integer tmp = numeric_cast_v<mp_integer>(lhs);
if(id==ID_lt)
++tmp;
integer_intervalt &ii=int_map[rhs_identifier];

View File

@ -123,10 +123,9 @@ std::string inv_object_storet::build_string(const exprt &expr) const
if(expr.get(ID_value)==ID_NULL)
return "0";
mp_integer i;
if(!to_integer(expr, i))
return integer2string(i);
const auto i = numeric_cast<mp_integer>(expr);
if(i.has_value())
return integer2string(*i);
}
// we also like "address_of" and "reference_to"
@ -455,25 +454,24 @@ void invariant_sett::strengthen_rec(const exprt &expr)
get_object(expr.op1(), p.second))
return;
mp_integer i0, i1;
bool have_i0=!to_integer(expr.op0(), i0);
bool have_i1=!to_integer(expr.op1(), i1);
const auto i0 = numeric_cast<mp_integer>(expr.op0());
const auto i1 = numeric_cast<mp_integer>(expr.op1());
if(expr.id()==ID_le)
{
if(have_i0)
add_bounds(p.second, lower_interval(i0));
else if(have_i1)
add_bounds(p.first, upper_interval(i1));
if(i0.has_value())
add_bounds(p.second, lower_interval(*i0));
else if(i1.has_value())
add_bounds(p.first, upper_interval(*i1));
else
add_le(p);
}
else if(expr.id()==ID_lt)
{
if(have_i0)
add_bounds(p.second, lower_interval(i0+1));
else if(have_i1)
add_bounds(p.first, upper_interval(i1-1));
if(i0.has_value())
add_bounds(p.second, lower_interval(*i0 + 1));
else if(i1.has_value())
add_bounds(p.first, upper_interval(*i1 - 1));
else
{
add_le(p);
@ -553,12 +551,12 @@ void invariant_sett::strengthen_rec(const exprt &expr)
get_object(expr.op1(), p.second))
return;
mp_integer i;
if(!to_integer(expr.op0(), i))
add_bounds(p.second, boundst(i));
else if(!to_integer(expr.op1(), i))
add_bounds(p.first, boundst(i));
const auto i0 = numeric_cast<mp_integer>(expr.op0());
const auto i1 = numeric_cast<mp_integer>(expr.op1());
if(i0.has_value())
add_bounds(p.second, boundst(*i0));
else if(i1.has_value())
add_bounds(p.first, boundst(*i1));
s=p;
std::swap(s.first, s.second);
@ -685,10 +683,10 @@ void invariant_sett::get_bounds(unsigned a, boundst &bounds) const
{
const exprt &e_a=object_store->get_expr(a);
mp_integer tmp;
if(!to_integer(e_a, tmp))
const auto tmp = numeric_cast<mp_integer>(e_a);
if(tmp.has_value())
{
bounds=boundst(tmp);
bounds = boundst(*tmp);
return;
}
@ -858,8 +856,7 @@ exprt invariant_sett::get_constant(const exprt &expr) const
if(e.is_constant())
{
mp_integer value;
assert(!to_integer(e, value));
const mp_integer value = numeric_cast_v<mp_integer>(e);
if(expr.type().id()==ID_pointer)
{

View File

@ -618,9 +618,7 @@ std::string expr2ct::convert_rec(
{
const vector_typet &vector_type=to_vector_type(src);
mp_integer size_int;
to_integer(vector_type.size(), size_int);
const mp_integer size_int = numeric_cast_v<mp_integer>(vector_type.size());
std::string dest="__gcc_v"+integer2string(size_int);
std::string tmp=convert(vector_type.subtype());

View File

@ -225,10 +225,7 @@ void cpp_typecheckt::zero_initializer(
if(size_expr.id()==ID_infinity)
return; // don't initialize
mp_integer size;
bool to_int=to_integer(size_expr, size);
CHECK_RETURN(!to_int);
const mp_integer size = numeric_cast_v<mp_integer>(size_expr);
CHECK_RETURN(size>=0);
exprt::operandst empty_operands;

View File

@ -203,13 +203,13 @@ std::string trace_numeric_value(
}
else if(type.id()==ID_integer)
{
mp_integer i;
if(!to_integer(expr, i) && i>=0)
const auto i = numeric_cast<mp_integer>(expr);
if(i.has_value() && *i >= 0)
{
if(options.hex_representation)
return "0x" + integer2string(i, 16);
return "0x" + integer2string(*i, 16);
else
return "0b" + integer2string(i, 2);
return "0b" + integer2string(*i, 2);
}
}
}

View File

@ -497,7 +497,7 @@ exprt interpretert::get_value(
}
else
{
to_integer(size_expr, count);
count = numeric_cast_v<mp_integer>(size_expr);
}
// Retrieve the value for each member in the array
@ -564,7 +564,7 @@ exprt interpretert::get_value(
}
else
{
to_integer(size_expr, count);
count = numeric_cast_v<mp_integer>(size_expr);
}
// Retrieve the value for each member in the array
@ -1023,9 +1023,7 @@ mp_integer interpretert::get_size(const typet &type)
// Go via the binary representation to reproduce any
// overflow behaviour.
exprt size_const=from_integer(i[0], size_expr.type());
mp_integer size_mp;
bool ret=to_integer(size_const, size_mp);
CHECK_RETURN(!ret);
const mp_integer size_mp = numeric_cast_v<mp_integer>(size_const);
return subtype_size*size_mp;
}
return subtype_size;

View File

@ -408,10 +408,9 @@ void interpretert::evaluate(
}
else
{
mp_integer i;
if(!to_integer(expr, i))
if(const auto i = numeric_cast<mp_integer>(expr))
{
dest.push_back(i);
dest.push_back(*i);
return;
}
}

View File

@ -91,8 +91,8 @@ static void remove_vector(exprt &expr)
remove_vector(expr.type());
array_typet array_type=to_array_type(expr.type());
mp_integer dimension;
to_integer(array_type.size(), dimension);
const mp_integer dimension =
numeric_cast_v<mp_integer>(array_type.size());
const typet subtype=array_type.subtype();
// do component-wise:
@ -118,8 +118,8 @@ static void remove_vector(exprt &expr)
remove_vector(expr.type());
array_typet array_type=to_array_type(expr.type());
mp_integer dimension;
to_integer(array_type.size(), dimension);
const mp_integer dimension =
numeric_cast_v<mp_integer>(array_type.size());
const typet subtype=array_type.subtype();
// do component-wise:

View File

@ -96,8 +96,7 @@ exprt get_quantifier_var_max(
if(expr_eq(var_expr, x.op0()) && x.op1().id()==ID_constant)
{
exprt over_expr=x.op1();
mp_integer over_i;
to_integer(over_expr, over_i);
mp_integer over_i = numeric_cast_v<mp_integer>(over_expr);
/**
* Due to the ''simplify'',
* the ''over_i'' value we obtain here is not the exact
@ -125,8 +124,7 @@ exprt get_quantifier_var_max(
if(expr_eq(var_expr, y.op0()) && y.op1().id()==ID_constant)
{
exprt over_expr=y.op1();
mp_integer over_i;
to_integer(over_expr, over_i);
mp_integer over_i = numeric_cast_v<mp_integer>(over_expr);
over_i-=1;
res=from_integer(over_i, y.op1().type());
return res;

View File

@ -84,13 +84,11 @@ void boolbvt::convert_update_rec(
std::size_t element_size=boolbv_width(subtype);
// iterate over array
mp_integer size;
if(to_integer(array_type.size(), size))
throw "update: failed to get array size";
const std::size_t size = numeric_cast_v<std::size_t>(array_type.size());
bvt tmp_bv=bv;
for(std::size_t i=0; i!=integer2size_t(size); ++i)
for(std::size_t i = 0; i != size; ++i)
{
std::size_t new_offset=offset+i*element_size;

View File

@ -31,6 +31,8 @@ void qdimacs_coret::simplify_extractbits(exprt &expr) const
}
}
// clang-format off
// this is unmaintained code, don't try to reformat it
for(used_bits_mapt::const_iterator it=used_bits_map.begin();
it!=used_bits_map.end();
it++)
@ -58,9 +60,8 @@ void qdimacs_coret::simplify_extractbits(exprt &expr) const
if(oit->op0().get(ID_identifier)==ident)
{
const exprt &val_expr=oit->op1();
mp_integer value;
to_integer(val_expr, value);
value_string[value.to_ulong()]='1';
const std::size_t value = numeric_cast_v<std::size_t>(val_expr);
value_string[value]='1';
#if 0
std::cout << "[" << value << "]=1\n";
@ -94,5 +95,6 @@ void qdimacs_coret::simplify_extractbits(exprt &expr) const
}
#endif
}
// clang-format on
}
}

View File

@ -185,11 +185,11 @@ void bv_refinementt::check_SAT(approximationt &a)
o1.unpack(a.op1_value);
// get actual rounding mode
mp_integer rounding_mode_int;
exprt rounding_mode_expr = get(a.expr.op2());
to_integer(rounding_mode_expr, rounding_mode_int);
const std::size_t rounding_mode_int =
numeric_cast_v<std::size_t>(rounding_mode_expr);
ieee_floatt::rounding_modet rounding_mode =
(ieee_floatt::rounding_modet)integer2ulong(rounding_mode_int);
(ieee_floatt::rounding_modet)rounding_mode_int;
ieee_floatt result=o0;
o0.rounding_mode=rounding_mode;

View File

@ -1525,10 +1525,7 @@ exprt simplify_exprt::bits2expr(
{
const array_typet &array_type=to_array_type(type);
mp_integer size;
if(to_integer(array_type.size(), size))
UNREACHABLE;
std::size_t n_el=integer2size_t(size);
const std::size_t n_el = numeric_cast_v<std::size_t>(array_type.size());
const auto el_size_opt = pointer_offset_bits(array_type.subtype(), ns);
CHECK_RETURN(el_size_opt.has_value() && *el_size_opt > 0);

View File

@ -31,8 +31,7 @@ bool simplify_exprt::simplify_bswap(bswap_exprt &expr)
{
auto bits_per_byte = expr.get_bits_per_byte();
std::size_t width=to_bitvector_type(expr.type()).get_width();
mp_integer value;
to_integer(expr.op(), value);
const mp_integer value = numeric_cast_v<mp_integer>(expr.op());
std::vector<mp_integer> bytes;
// take apart
@ -1788,8 +1787,7 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr)
if(changed)
{
// adjust constant
mp_integer i;
to_integer(expr.op1(), i);
mp_integer i = numeric_cast_v<mp_integer>(expr.op1());
i-=constant;
expr.op1()=from_integer(i, expr.op1().type());

View File

@ -35,10 +35,7 @@ static void build_ssa_identifier_rec(
build_ssa_identifier_rec(index.array(), l0, l1, l2, os, l1_object_os);
mp_integer idx;
if(to_integer(to_constant_expr(index.index()), idx))
UNREACHABLE;
const mp_integer idx = numeric_cast_v<mp_integer>(index.index());
os << '[' << idx << ']';
}
else if(expr.id()==ID_symbol)

View File

@ -247,8 +247,7 @@ xmlt xml(
result.name="integer";
result.set_attribute("c_type", "_Bool");
result.set_attribute("binary", expr.get_string(ID_value));
mp_integer b;
to_integer(to_constant_expr(expr), b);
const mp_integer b = numeric_cast_v<mp_integer>(expr);
result.data=integer2string(b);
}
else

View File

@ -28,9 +28,8 @@ index_exprt require_expr::require_index(const exprt &expr, int expected_index)
REQUIRE(expr.id()==ID_index);
const index_exprt &index_expr=to_index_expr(expr);
REQUIRE(index_expr.index().id()==ID_constant);
const constant_exprt &index_value=to_constant_expr(index_expr.index());
mp_integer index_integer_value;
to_integer(index_value, index_integer_value);
const mp_integer index_integer_value =
numeric_cast_v<mp_integer>(index_expr.index());
REQUIRE(index_integer_value==expected_index);
return index_expr;

View File

@ -36,8 +36,7 @@ TEST_CASE("Simplify pointer_offset(address of array index)")
exprt simp=simplify_expr(p_o, ns);
REQUIRE(simp.id()==ID_constant);
mp_integer offset_value;
REQUIRE(!to_integer(simp, offset_value));
const mp_integer offset_value = numeric_cast_v<mp_integer>(simp);
REQUIRE(offset_value==1);
}
@ -57,8 +56,7 @@ TEST_CASE("Simplify const pointer offset")
exprt simp=simplify_expr(p_o, ns);
REQUIRE(simp.id()==ID_constant);
mp_integer offset_value;
REQUIRE(!to_integer(simp, offset_value));
const mp_integer offset_value = numeric_cast_v<mp_integer>(simp);
REQUIRE(offset_value==1234);
}