Skip to content

Commit dd50d12

Browse files
committed
Use appropriate numeric_cast_v<T> instead of deprecated integer2unsigned
This includes several type fixes - only three instances ended up as numeric_cast_v<unsigned>, all others uses of integer2unsigned were actually in contexts where some other type was required.
1 parent ed4637b commit dd50d12

12 files changed

+28
-27
lines changed

src/ansi-c/expr2c.cpp

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2219,10 +2219,7 @@ std::string expr2ct::convert_array(
22192219
if(it==--src.operands().end())
22202220
break;
22212221

2222-
assert(it->is_constant());
2223-
mp_integer i;
2224-
to_integer(*it, i);
2225-
unsigned int ch=integer2unsigned(i);
2222+
const unsigned int ch = numeric_cast_v<unsigned>(*it);
22262223

22272224
if(last_was_hex)
22282225
{

src/solvers/flattening/boolbv.cpp

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -74,7 +74,8 @@ bool boolbvt::literal(
7474
if(to_integer(index_expr.index(), index))
7575
throw "literal expects constant index";
7676

77-
std::size_t offset=integer2unsigned(index*element_width);
77+
const std::size_t offset =
78+
numeric_cast_v<std::size_t>(index * element_width);
7879

7980
return literal(index_expr.array(), bit+offset, dest);
8081
}
@@ -358,7 +359,7 @@ bvt boolbvt::convert_lambda(const exprt &expr)
358359

359360
const bvt &tmp=convert_bv(expr_op1);
360361

361-
std::size_t offset=integer2unsigned(i*tmp.size());
362+
const std::size_t offset = numeric_cast_v<std::size_t>(i * tmp.size());
362363

363364
if(size*tmp.size()!=width)
364365
throw "convert_lambda: unexpected operand width";

src/solvers/flattening/boolbv_byte_update.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -60,7 +60,7 @@ bvt boolbvt::convert_byte_update(const byte_update_exprt &expr)
6060
bv_endianness_mapt map_op(op.type(), false, ns, boolbv_width);
6161
bv_endianness_mapt map_value(value.type(), false, ns, boolbv_width);
6262

63-
std::size_t offset_i=integer2unsigned(offset);
63+
const std::size_t offset_i = numeric_cast_v<std::size_t>(offset);
6464

6565
for(std::size_t i=0; i<update_width; i++)
6666
{

src/solvers/flattening/boolbv_extractbits.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -61,7 +61,7 @@ bvt boolbvt::convert_extractbits(const extractbits_exprt &expr)
6161
throw 0;
6262
}
6363

64-
std::size_t offset=integer2unsigned(o2);
64+
const std::size_t offset = numeric_cast_v<std::size_t>(o2);
6565

6666
bvt bv;
6767
bv.resize(width);

src/solvers/flattening/boolbv_replication.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,7 @@ bvt boolbvt::convert_replication(const replication_exprt &expr)
2424
bvt bv;
2525
bv.resize(width);
2626

27-
const std::size_t u_times=integer2unsigned(times);
27+
const std::size_t u_times = numeric_cast_v<std::size_t>(times);
2828
const bvt &op=convert_bv(expr.op1());
2929
std::size_t offset=0;
3030

src/solvers/flattening/boolbv_width.cpp

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -144,7 +144,7 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
144144
if(total>(1<<30)) // realistic limit
145145
throw "array too large for flattening";
146146

147-
entry.total_width=integer2unsigned(total);
147+
entry.total_width = numeric_cast_v<std::size_t>(total);
148148
}
149149
}
150150
else if(type_id==ID_vector)
@@ -165,13 +165,13 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
165165
if(total>(1<<30)) // realistic limit
166166
throw "vector too large for flattening";
167167

168-
entry.total_width=integer2unsigned(vector_size*sub_width);
168+
entry.total_width = numeric_cast_v<std::size_t>(vector_size * sub_width);
169169
}
170170
}
171171
else if(type_id==ID_complex)
172172
{
173-
std::size_t sub_width=operator()(type.subtype());
174-
entry.total_width=integer2unsigned(2*sub_width);
173+
const mp_integer sub_width = operator()(type.subtype());
174+
entry.total_width = numeric_cast_v<std::size_t>(2 * sub_width);
175175
}
176176
else if(type_id==ID_code)
177177
{

src/solvers/flattening/boolbv_with.cpp

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -146,7 +146,8 @@ void boolbvt::convert_with_array(
146146

147147
if(op1_value>=0 && op1_value<size) // bounds check
148148
{
149-
std::size_t offset=integer2unsigned(op1_value*op2_bv.size());
149+
const std::size_t offset =
150+
numeric_cast_v<std::size_t>(op1_value * op2_bv.size());
150151

151152
for(std::size_t j=0; j<op2_bv.size(); j++)
152153
next_bv[offset+j]=op2_bv[j];
@@ -163,7 +164,7 @@ void boolbvt::convert_with_array(
163164

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

166-
std::size_t offset=integer2unsigned(i*op2_bv.size());
167+
const std::size_t offset = numeric_cast_v<std::size_t>(i * op2_bv.size());
167168

168169
for(std::size_t j=0; j<op2_bv.size(); j++)
169170
next_bv[offset+j]=

src/solvers/flattening/flatten_byte_operators.cpp

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -315,7 +315,7 @@ exprt flatten_byte_extract(
315315
const typet &offset_type=ns.follow(offset.type());
316316

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

@@ -543,11 +543,13 @@ exprt flatten_byte_update(
543543
// zero-extend the value, but only if needed
544544
exprt value_extended;
545545

546-
if(width>integer2unsigned(element_size)*8)
546+
if(width > element_size * 8)
547547
value_extended=
548548
concatenation_exprt(
549549
from_integer(
550-
0, unsignedbv_typet(width-integer2unsigned(element_size)*8)),
550+
0,
551+
unsignedbv_typet(
552+
width - numeric_cast_v<std::size_t>(element_size * 8))),
551553
src.op2(), t);
552554
else
553555
value_extended=src.op2();

src/solvers/qbf/qbf_qube_core.cpp

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@ Author: CM Wintersteiger
1212
#include <cstring>
1313
#include <fstream>
1414

15+
#include <util/arith_tools.h>
1516
#include <util/invariant.h>
1617
#include <util/mp_arith.h>
1718

@@ -78,9 +79,9 @@ propt::resultt qbf_qube_coret::prop_solve()
7879
{
7980
mp_integer b(line.substr(2).c_str());
8081
if(b<0)
81-
assignment[integer2unsigned(b.negate())]=false;
82+
assignment[numeric_cast_v<std::size_t>(b.negate())] = false;
8283
else
83-
assignment[integer2unsigned(b)]=true;
84+
assignment[numeric_cast_v<std::size_t>(b)] = true;
8485
}
8586
else if(line=="s cnf 1")
8687
{

src/util/arith_tools.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -100,7 +100,7 @@ bool to_unsigned_integer(const constant_exprt &expr, unsigned &uint_value)
100100
return true;
101101
else
102102
{
103-
uint_value=integer2unsigned(i);
103+
uint_value = numeric_cast_v<unsigned>(i);
104104
return false;
105105
}
106106
}

src/util/config.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1136,7 +1136,7 @@ static unsigned unsigned_from_ns(
11361136
"symbol table configuration entry `" + id2string(id) +
11371137
"' must be convertible to mp_integer");
11381138

1139-
return integer2unsigned(int_value);
1139+
return numeric_cast_v<unsigned>(int_value);
11401140
}
11411141

11421142
void configt::set_from_symbol_table(

src/util/string_constant.cpp

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -87,13 +87,12 @@ bool string_constantt::from_array_expr(const array_exprt &src)
8787

8888
std::string value;
8989

90-
forall_operands(it, src)
90+
for(const auto &op : src.operands())
9191
{
92-
mp_integer int_value=0;
93-
if(to_integer(*it, int_value))
92+
if(!op.is_constant())
9493
return true;
95-
unsigned unsigned_value=integer2unsigned(int_value);
96-
value+=static_cast<char>(unsigned_value);
94+
95+
value += numeric_cast_v<char>(op);
9796
}
9897

9998
// Drop the implicit zero at the end.

0 commit comments

Comments
 (0)