Skip to content

Commit 88d1718

Browse files
committed
Deprecate get_unsigned_int
Using "unsigned" is almost always wrong - the type is unrelated to both the machine type the code is compiled on as well as the width of the platform we are running an analysis for. get_unsigned_int specifically was used inconsistently: the same entry (ID_width) is set via APIs with a parameter of type size_t and several places already used get_size_t.
1 parent 62ec461 commit 88d1718

File tree

12 files changed

+27
-27
lines changed

12 files changed

+27
-27
lines changed

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

+12-12
Original file line numberDiff line numberDiff line change
@@ -707,9 +707,9 @@ void java_bytecode_convert_methodt::replace_goto_target(
707707
code_blockt &java_bytecode_convert_methodt::get_block_for_pcrange(
708708
block_tree_nodet &tree,
709709
code_blockt &this_block,
710-
unsigned address_start,
711-
unsigned address_limit,
712-
unsigned next_block_start_address)
710+
std::size_t address_start,
711+
std::size_t address_limit,
712+
std::size_t next_block_start_address)
713713
{
714714
address_mapt dummy;
715715
return get_or_create_block_for_pcrange(
@@ -739,9 +739,9 @@ code_blockt &java_bytecode_convert_methodt::get_block_for_pcrange(
739739
code_blockt &java_bytecode_convert_methodt::get_or_create_block_for_pcrange(
740740
block_tree_nodet &tree,
741741
code_blockt &this_block,
742-
unsigned address_start,
743-
unsigned address_limit,
744-
unsigned next_block_start_address,
742+
std::size_t address_start,
743+
std::size_t address_limit,
744+
std::size_t next_block_start_address,
745745
const address_mapt &amap,
746746
bool allow_merge)
747747
{
@@ -771,7 +771,7 @@ code_blockt &java_bytecode_convert_methodt::get_or_create_block_for_pcrange(
771771
tree.branch_addresses.begin(),
772772
tree.branch_addresses.end(),
773773
address_limit);
774-
unsigned findlim_block_start_address=
774+
const auto findlim_block_start_address =
775775
findlim==tree.branch_addresses.end() ?
776776
next_block_start_address :
777777
(*findlim);
@@ -917,7 +917,7 @@ code_blockt &java_bytecode_convert_methodt::get_or_create_block_for_pcrange(
917917
}
918918

919919
static void gather_symbol_live_ranges(
920-
unsigned pc,
920+
std::size_t pc,
921921
const exprt &e,
922922
std::map<irep_idt, java_bytecode_convert_methodt::variablet> &result)
923923
{
@@ -974,11 +974,11 @@ codet java_bytecode_convert_methodt::get_clinit_call(
974974
}
975975
}
976976

977-
static unsigned get_bytecode_type_width(const typet &ty)
977+
static std::size_t get_bytecode_type_width(const typet &ty)
978978
{
979979
if(ty.id()==ID_pointer)
980980
return 32;
981-
return ty.get_unsigned_int(ID_width);
981+
return ty.get_size_t(ID_width);
982982
}
983983

984984
codet java_bytecode_convert_methodt::convert_instructions(
@@ -1046,7 +1046,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
10461046
{
10471047
const std::vector<unsigned int> handler =
10481048
try_catch_handler(i_it->address, method.exception_table);
1049-
std::list<unsigned int> &successors = a_entry.first->second.successors;
1049+
std::list<std::size_t> &successors = a_entry.first->second.successors;
10501050
successors.insert(successors.end(), handler.begin(), handler.end());
10511051
targets.insert(handler.begin(), handler.end());
10521052
}
@@ -1692,7 +1692,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
16921692
push(results);
16931693

16941694
instruction.done = true;
1695-
for(const unsigned address : instruction.successors)
1695+
for(const auto address : instruction.successors)
16961696
{
16971697
address_mapt::iterator a_it2=address_map.find(address);
16981698
CHECK_RETURN(a_it2 != address_map.end());

jbmc/src/java_bytecode/java_utils.cpp

+1-3
Original file line numberDiff line numberDiff line change
@@ -34,9 +34,7 @@ unsigned java_local_variable_slots(const typet &t)
3434
if(t.id()==ID_pointer)
3535
return 1;
3636

37-
unsigned bitwidth;
38-
39-
bitwidth=t.get_unsigned_int(ID_width);
37+
const std::size_t bitwidth = t.get_size_t(ID_width);
4038
INVARIANT(
4139
bitwidth==8 ||
4240
bitwidth==16 ||

src/ansi-c/c_typecast.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -277,7 +277,7 @@ typet c_typecastt::follow_with_qualifiers(const typet &src_type)
277277
c_typecastt::c_typet c_typecastt::get_c_type(
278278
const typet &type) const
279279
{
280-
unsigned width=type.get_int(ID_width);
280+
const std::size_t width = type.get_size_t(ID_width);
281281

282282
if(type.id()==ID_signedbv)
283283
{

src/ansi-c/c_typecheck_type.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -1368,7 +1368,7 @@ void c_typecheck_baset::typecheck_c_bit_field_type(c_bit_field_typet &type)
13681368
throw 0;
13691369
}
13701370

1371-
sub_width=c_enum_type.subtype().get_int(ID_width);
1371+
sub_width = c_enum_type.subtype().get_size_t(ID_width);
13721372
}
13731373
else
13741374
{

src/ansi-c/padding.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -124,7 +124,7 @@ underlying_width(const c_bit_field_typet &type, const namespacet &ns)
124124
const typet &c_enum_type = ns.follow_tag(to_c_enum_tag_type(subtype));
125125

126126
if(c_enum_type.id() == ID_c_enum)
127-
return c_enum_type.subtype().get_int(ID_width);
127+
return c_enum_type.subtype().get_size_t(ID_width);
128128
else
129129
return {};
130130
}

src/goto-instrument/accelerate/overflow_instrumenter.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -110,8 +110,8 @@ void overflow_instrumentert::overflow_expr(
110110
}
111111

112112
const typet &old_type=ns.follow(expr.op0().type());
113-
std::size_t new_width=expr.type().get_int(ID_width);
114-
std::size_t old_width=old_type.get_int(ID_width);
113+
const std::size_t new_width = expr.type().get_size_t(ID_width);
114+
const std::size_t old_width = old_type.get_size_t(ID_width);
115115

116116
if(type.id()==ID_signedbv)
117117
{

src/solvers/flattening/boolbv_not.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ bvt boolbvt::convert_not(const not_exprt &expr)
2323
{
2424
if((expr.type().id()==ID_verilog_signedbv ||
2525
expr.type().id()==ID_verilog_unsignedbv) &&
26-
expr.type().get_int(ID_width)==1)
26+
expr.type().get_size_t(ID_width) == 1)
2727
{
2828
literalt has_x_or_z=bv_utils.verilog_bv_has_x_or_z(op_bv);
2929
literalt normal_bits_zero=

src/solvers/flattening/boolbv_reduction.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -76,7 +76,7 @@ bvt boolbvt::convert_bv_reduction(const unary_exprt &expr)
7676
{
7777
if((expr.type().id()==ID_verilog_signedbv ||
7878
expr.type().id()==ID_verilog_unsignedbv) &&
79-
expr.type().get_int(ID_width)==1)
79+
expr.type().get_size_t(ID_width) == 1)
8080
{
8181
bvt bv;
8282
bv.resize(2);

src/solvers/flattening/boolbv_width.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -110,7 +110,7 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
110110
type_id==ID_verilog_unsignedbv)
111111
{
112112
// we encode with two bits
113-
entry.total_width=type.get_unsigned_int(ID_width)*2;
113+
entry.total_width = type.get_size_t(ID_width) * 2;
114114
assert(entry.total_width!=0);
115115
}
116116
else if(type_id==ID_range)
@@ -186,7 +186,7 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
186186
else if(type_id==ID_c_enum)
187187
{
188188
// these have a subtype
189-
entry.total_width=type.subtype().get_unsigned_int(ID_width);
189+
entry.total_width = type.subtype().get_size_t(ID_width);
190190
assert(entry.total_width!=0);
191191
}
192192
else if(type_id==ID_incomplete_c_enum)

src/util/arith_tools.cpp

+2-1
Original file line numberDiff line numberDiff line change
@@ -152,7 +152,8 @@ constant_exprt from_integer(
152152
}
153153
else if(type_id==ID_c_enum)
154154
{
155-
std::size_t width=to_c_enum_type(type).subtype().get_unsigned_int(ID_width);
155+
const std::size_t width =
156+
to_c_enum_type(type).subtype().get_size_t(ID_width);
156157
constant_exprt result(type);
157158
result.set_value(integer2binary(int_value, width));
158159
return result;

src/util/irep.h

+3
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
1414
#include <string>
1515
#include <vector>
1616

17+
#include "deprecate.h"
1718
#include "irep_ids.h"
1819

1920
#define SHARING
@@ -207,6 +208,8 @@ class irept
207208
const irep_idt &get(const irep_namet &name) const;
208209
bool get_bool(const irep_namet &name) const;
209210
signed int get_int(const irep_namet &name) const;
211+
/// \deprecated use get_size_t instead
212+
DEPRECATED("Use get_size_t instead")
210213
unsigned int get_unsigned_int(const irep_namet &name) const;
211214
std::size_t get_size_t(const irep_namet &name) const;
212215
long long get_long_long(const irep_namet &name) const;

unit/util/irep.cpp

-2
Original file line numberDiff line numberDiff line change
@@ -185,7 +185,6 @@ SCENARIO("irept_memory", "[core][utils][irept]")
185185
// variants in the API
186186
REQUIRE(!irep.get_bool("no_such_id"));
187187
REQUIRE(irep.get_int("no_such_id") == 0);
188-
REQUIRE(irep.get_unsigned_int("no_such_id") == 0u);
189188
REQUIRE(irep.get_size_t("no_such_id") == 0u);
190189
REQUIRE(irep.get_long_long("no_such_id") == 0);
191190

@@ -199,7 +198,6 @@ SCENARIO("irept_memory", "[core][utils][irept]")
199198
irep.set("numeric_id", 42);
200199
REQUIRE(!irep.get_bool("numeric_id"));
201200
REQUIRE(irep.get_int("numeric_id") == 42);
202-
REQUIRE(irep.get_unsigned_int("numeric_id") == 42u);
203201
REQUIRE(irep.get_size_t("numeric_id") == 42u);
204202
REQUIRE(irep.get_long_long("numeric_id") == 42);
205203

0 commit comments

Comments
 (0)