Skip to content

Commit 0afc778

Browse files
committed
Use numeric_cast<mp_integer> instead of deprecated to_integer variants
to_integer should only be used with a constant_exprt as first argument. Includes a bugfix in goto_rw where the result of pointer_offset_bits did not have operator* applied.
1 parent b1c0b87 commit 0afc778

20 files changed

+226
-229
lines changed

src/analyses/goto_rw.cpp

+5-6
Original file line numberDiff line numberDiff line change
@@ -150,22 +150,21 @@ void rw_range_sett::get_objects_byte_extract(
150150
{
151151
const exprt simp_offset=simplify_expr(be.offset(), ns);
152152

153-
mp_integer index;
154-
if(range_start==-1 || to_integer(simp_offset, index))
153+
auto index = numeric_cast<mp_integer>(simp_offset);
154+
if(range_start==-1 || !index.has_value())
155155
get_objects_rec(mode, be.op(), -1, size);
156156
else
157157
{
158-
index*=8;
159-
if(index>=pointer_offset_bits(be.op().type(), ns))
158+
*index *= 8;
159+
if(*index >= *pointer_offset_bits(be.op().type(), ns))
160160
return;
161161

162162
endianness_mapt map(
163163
be.op().type(),
164164
be.id()==ID_byte_extract_little_endian,
165165
ns);
166-
assert(index<std::numeric_limits<size_t>::max());
167166
range_spect offset =
168-
range_start + map.map_bit(numeric_cast_v<std::size_t>(index));
167+
range_start + map.map_bit(numeric_cast_v<std::size_t>(*index));
169168
get_objects_rec(mode, be.op(), offset, size);
170169
}
171170
}

src/ansi-c/c_typecheck_expr.cpp

+5-4
Original file line numberDiff line numberDiff line change
@@ -2896,12 +2896,13 @@ bool c_typecheck_baset::gcc_vector_types_compatible(
28962896
// This is relatively restrictive!
28972897

28982898
// compare dimension
2899-
mp_integer s0, s1;
2900-
if(to_integer(type0.size(), s0))
2899+
const auto s0 = numeric_cast<mp_integer>(type0.size());
2900+
const auto s1 = numeric_cast<mp_integer>(type1.size());
2901+
if(!s0.has_value())
29012902
return false;
2902-
if(to_integer(type1.size(), s1))
2903+
if(!s1.has_value())
29032904
return false;
2904-
if(s0!=s1)
2905+
if(*s0!=*s1)
29052906
return false;
29062907

29072908
// compare subtype

src/ansi-c/c_typecheck_initializer.cpp

+23-22
Original file line numberDiff line numberDiff line change
@@ -91,29 +91,29 @@ exprt c_typecheck_baset::do_initializer_rec(
9191
to_array_type(full_type).is_complete())
9292
{
9393
// check size
94-
mp_integer array_size;
95-
if(to_integer(to_array_type(full_type).size(), array_size))
94+
const auto array_size = numeric_cast<mp_integer>(to_array_type(full_type).size());
95+
if(!array_size.has_value())
9696
{
9797
error().source_location = value.source_location();
9898
error() << "array size needs to be constant, got "
9999
<< to_string(to_array_type(full_type).size()) << eom;
100100
throw 0;
101101
}
102102

103-
if(array_size<0)
103+
if(*array_size<0)
104104
{
105105
error().source_location = value.source_location();
106106
error() << "array size must not be negative" << eom;
107107
throw 0;
108108
}
109109

110-
if(mp_integer(tmp.operands().size())>array_size)
110+
if(mp_integer(tmp.operands().size())>*array_size)
111111
{
112112
// cut off long strings. gcc does a warning for this
113-
tmp.operands().resize(numeric_cast_v<std::size_t>(array_size));
113+
tmp.operands().resize(numeric_cast_v<std::size_t>(*array_size));
114114
tmp.type()=type;
115115
}
116-
else if(mp_integer(tmp.operands().size())<array_size)
116+
else if(mp_integer(tmp.operands().size())<*array_size)
117117
{
118118
// fill up
119119
tmp.type()=type;
@@ -126,7 +126,7 @@ exprt c_typecheck_baset::do_initializer_rec(
126126
<< to_string(full_type.subtype()) << "'" << eom;
127127
throw 0;
128128
}
129-
tmp.operands().resize(numeric_cast_v<std::size_t>(array_size), *zero);
129+
tmp.operands().resize(numeric_cast_v<std::size_t>(*array_size), *zero);
130130
}
131131
}
132132

@@ -152,29 +152,29 @@ exprt c_typecheck_baset::do_initializer_rec(
152152
to_array_type(full_type).is_complete())
153153
{
154154
// check size
155-
mp_integer array_size;
156-
if(to_integer(to_array_type(full_type).size(), array_size))
155+
const auto array_size = numeric_cast<mp_integer>(to_array_type(full_type).size());
156+
if(!array_size.has_value())
157157
{
158158
error().source_location = value.source_location();
159159
error() << "array size needs to be constant, got "
160160
<< to_string(to_array_type(full_type).size()) << eom;
161161
throw 0;
162162
}
163163

164-
if(array_size<0)
164+
if(*array_size<0)
165165
{
166166
error().source_location = value.source_location();
167167
error() << "array size must not be negative" << eom;
168168
throw 0;
169169
}
170170

171-
if(mp_integer(tmp2.operands().size())>array_size)
171+
if(mp_integer(tmp2.operands().size())>*array_size)
172172
{
173173
// cut off long strings. gcc does a warning for this
174-
tmp2.operands().resize(numeric_cast_v<std::size_t>(array_size));
174+
tmp2.operands().resize(numeric_cast_v<std::size_t>(*array_size));
175175
tmp2.type()=type;
176176
}
177-
else if(mp_integer(tmp2.operands().size())<array_size)
177+
else if(mp_integer(tmp2.operands().size())<*array_size)
178178
{
179179
// fill up
180180
tmp2.type()=type;
@@ -187,7 +187,7 @@ exprt c_typecheck_baset::do_initializer_rec(
187187
<< to_string(full_type.subtype()) << "'" << eom;
188188
throw 0;
189189
}
190-
tmp2.operands().resize(numeric_cast_v<std::size_t>(array_size), *zero);
190+
tmp2.operands().resize(numeric_cast_v<std::size_t>(*array_size), *zero);
191191
}
192192
}
193193

@@ -319,35 +319,34 @@ void c_typecheck_baset::designator_enter(
319319
}
320320
else
321321
{
322-
mp_integer array_size;
323-
324-
if(to_integer(array_type.size(), array_size))
322+
const auto array_size = numeric_cast<mp_integer>(array_type.size());
323+
if(!array_size.has_value())
325324
{
326325
error().source_location = array_type.size().source_location();
327326
error() << "array has non-constant size `"
328327
<< to_string(array_type.size()) << "'" << eom;
329328
throw 0;
330329
}
331330

332-
entry.size = numeric_cast_v<std::size_t>(array_size);
331+
entry.size = numeric_cast_v<std::size_t>(*array_size);
333332
entry.subtype=array_type.subtype();
334333
}
335334
}
336335
else if(full_type.id()==ID_vector)
337336
{
338337
const vector_typet &vector_type=to_vector_type(full_type);
339338

340-
mp_integer vector_size;
339+
const auto vector_size = numeric_cast<mp_integer>(vector_type.size());
341340

342-
if(to_integer(vector_type.size(), vector_size))
341+
if(!vector_size.has_value())
343342
{
344343
error().source_location = vector_type.size().source_location();
345344
error() << "vector has non-constant size `"
346345
<< to_string(vector_type.size()) << "'" << eom;
347346
throw 0;
348347
}
349348

350-
entry.size = numeric_cast_v<std::size_t>(vector_size);
349+
entry.size = numeric_cast_v<std::size_t>(*vector_size);
351350
entry.subtype=vector_type.subtype();
352351
}
353352
else
@@ -735,7 +734,9 @@ designatort c_typecheck_baset::make_designator(
735734

736735
if(to_array_type(full_type).size().is_nil())
737736
size=0;
738-
else if(to_integer(to_array_type(full_type).size(), size))
737+
else if(const auto size_opt = numeric_cast<mp_integer>(to_array_type(full_type).size()))
738+
size = *size_opt;
739+
else
739740
{
740741
error().source_location = d_op.op0().source_location();
741742
error() << "expected constant array size" << eom;

src/ansi-c/c_typecheck_type.cpp

+6-6
Original file line numberDiff line numberDiff line change
@@ -688,17 +688,17 @@ void c_typecheck_baset::typecheck_vector_type(vector_typet &type)
688688

689689
simplify(size_expr, *this);
690690

691-
mp_integer sub_size;
691+
const auto sub_size = numeric_cast<mp_integer>(size_expr);
692692

693-
if(to_integer(size_expr, sub_size))
693+
if(!sub_size.has_value())
694694
{
695695
error().source_location=source_location;
696696
error() << "failed to determine size of vector base type `"
697697
<< to_string(type.subtype()) << "'" << eom;
698698
throw 0;
699699
}
700700

701-
if(sub_size==0)
701+
if(*sub_size==0)
702702
{
703703
error().source_location=source_location;
704704
error() << "type had size 0: `"
@@ -707,16 +707,16 @@ void c_typecheck_baset::typecheck_vector_type(vector_typet &type)
707707
}
708708

709709
// adjust by width of base type
710-
if(s%sub_size!=0)
710+
if(s% *sub_size!=0)
711711
{
712712
error().source_location=source_location;
713713
error() << "vector size (" << s
714-
<< ") expected to be multiple of base type size (" << sub_size
714+
<< ") expected to be multiple of base type size (" << *sub_size
715715
<< ")" << eom;
716716
throw 0;
717717
}
718718

719-
s/=sub_size;
719+
s/= *sub_size;
720720

721721
type.size()=from_integer(s, signed_size_type());
722722
}

src/cpp/cpp_typecheck_initializer.cpp

+4-4
Original file line numberDiff line numberDiff line change
@@ -270,12 +270,12 @@ void cpp_typecheckt::zero_initializer(
270270

271271
exprt component_size=size_of_expr(component.type(), *this);
272272

273-
mp_integer size_int;
274-
if(!to_integer(component_size, size_int))
273+
const auto size_int = numeric_cast<mp_integer>(component_size);
274+
if(size_int.has_value())
275275
{
276-
if(size_int>max_comp_size)
276+
if(*size_int>max_comp_size)
277277
{
278-
max_comp_size=size_int;
278+
max_comp_size=*size_int;
279279
comp=component;
280280
}
281281
}

src/cpp/cpp_typecheck_resolve.cpp

+14-12
Original file line numberDiff line numberDiff line change
@@ -696,16 +696,16 @@ exprt cpp_typecheck_resolvet::do_builtin(
696696

697697
resolve_argument(argument, fargs);
698698

699-
mp_integer i;
700-
if(to_integer(argument, i))
699+
const auto i = numeric_cast<mp_integer>(argument);
700+
if(!i.has_value())
701701
{
702702
cpp_typecheck.error().source_location=source_location;
703703
cpp_typecheck.error() << "template argument must be constant"
704704
<< messaget::eom;
705705
throw 0;
706706
}
707707

708-
if(i<1)
708+
if(*i<1)
709709
{
710710
cpp_typecheck.error().source_location=source_location;
711711
cpp_typecheck.error()
@@ -715,7 +715,7 @@ exprt cpp_typecheck_resolvet::do_builtin(
715715
}
716716

717717
dest=type_exprt(typet(base_name));
718-
dest.type().set(ID_width, integer2string(i));
718+
dest.type().set(ID_width, integer2string(*i));
719719
}
720720
else if(base_name==ID_fixedbv)
721721
{
@@ -751,25 +751,27 @@ exprt cpp_typecheck_resolvet::do_builtin(
751751
throw 0;
752752
}
753753

754-
mp_integer width, integer_bits;
754+
const auto width = numeric_cast<mp_integer>(argument0);
755755

756-
if(to_integer(argument0, width))
756+
if(!width.has_value())
757757
{
758758
cpp_typecheck.error().source_location=argument0.find_source_location();
759759
cpp_typecheck.error() << "template argument must be constant"
760760
<< messaget::eom;
761761
throw 0;
762762
}
763763

764-
if(to_integer(argument1, integer_bits))
764+
const auto integer_bits = numeric_cast<mp_integer>(argument1);
765+
766+
if(!integer_bits.has_value())
765767
{
766768
cpp_typecheck.error().source_location=argument1.find_source_location();
767769
cpp_typecheck.error() << "template argument must be constant"
768770
<< messaget::eom;
769771
throw 0;
770772
}
771773

772-
if(width<1)
774+
if(*width<1)
773775
{
774776
cpp_typecheck.error().source_location=argument0.find_source_location();
775777
cpp_typecheck.error()
@@ -778,7 +780,7 @@ exprt cpp_typecheck_resolvet::do_builtin(
778780
throw 0;
779781
}
780782

781-
if(integer_bits<0)
783+
if(*integer_bits<0)
782784
{
783785
cpp_typecheck.error().source_location=argument1.find_source_location();
784786
cpp_typecheck.error()
@@ -787,7 +789,7 @@ exprt cpp_typecheck_resolvet::do_builtin(
787789
throw 0;
788790
}
789791

790-
if(integer_bits>width)
792+
if(*integer_bits > *width)
791793
{
792794
cpp_typecheck.error().source_location=argument1.find_source_location();
793795
cpp_typecheck.error()
@@ -797,8 +799,8 @@ exprt cpp_typecheck_resolvet::do_builtin(
797799
}
798800

799801
dest=type_exprt(typet(base_name));
800-
dest.type().set(ID_width, integer2string(width));
801-
dest.type().set(ID_integer_bits, integer2string(integer_bits));
802+
dest.type().set(ID_width, integer2string(*width));
803+
dest.type().set(ID_integer_bits, integer2string(*integer_bits));
802804
}
803805
else if(base_name==ID_integer)
804806
{

src/goto-programs/string_abstraction.cpp

+8-8
Original file line numberDiff line numberDiff line change
@@ -844,17 +844,17 @@ bool string_abstractiont::build_array(const array_exprt &object,
844844
return true;
845845

846846
const exprt &a_size=to_array_type(object.type()).size();
847-
mp_integer size;
847+
const auto size = numeric_cast<mp_integer>(a_size);
848848
// don't do anything, if we cannot determine the size
849-
if(to_integer(a_size, size))
849+
if(!size.has_value())
850850
return true;
851851
INVARIANT(
852-
size == object.operands().size(), "wrong number of array object arguments");
852+
*size == object.operands().size(), "wrong number of array object arguments");
853853

854854
exprt::operandst::const_iterator it=object.operands().begin();
855-
for(mp_integer i=0; i<size; ++i, ++it)
855+
for(mp_integer i=0; i<*size; ++i, ++it)
856856
if(it->is_zero())
857-
return build_symbol_constant(i, size, dest);
857+
return build_symbol_constant(i, *size, dest);
858858

859859
return true;
860860
}
@@ -1219,11 +1219,11 @@ goto_programt::targett string_abstractiont::value_assignments(
12191219
if(lhs.type().id()==ID_array)
12201220
{
12211221
const exprt &a_size=to_array_type(lhs.type()).size();
1222-
mp_integer size;
1222+
const auto size = numeric_cast<mp_integer>(a_size);
12231223
// don't do anything, if we cannot determine the size
1224-
if(to_integer(a_size, size))
1224+
if(!size.has_value())
12251225
return target;
1226-
for(mp_integer i=0; i<size; ++i)
1226+
for(mp_integer i=0; i<*size; ++i)
12271227
target=value_assignments(dest, target,
12281228
index_exprt(lhs, from_integer(i, a_size.type())),
12291229
index_exprt(rhs, from_integer(i, a_size.type())));

0 commit comments

Comments
 (0)