@@ -501,7 +501,7 @@ exprt interpretert::get_value(
501
501
}
502
502
503
503
// Retrieve the value for each member in the array
504
- result.reserve_operands (integer2size_t (count));
504
+ result.reserve_operands (numeric_cast_v<std:: size_t > (count));
505
505
for (mp_integer i=0 ; i<count; ++i)
506
506
{
507
507
const exprt operand=get_value (
@@ -568,7 +568,7 @@ exprt interpretert::get_value(
568
568
}
569
569
570
570
// Retrieve the value for each member in the array
571
- result.reserve_operands (integer2size_t (count));
571
+ result.reserve_operands (numeric_cast_v<std:: size_t > (count));
572
572
for (mp_integer i=0 ; i<count; ++i)
573
573
{
574
574
const exprt operand=get_value (type.subtype (), rhs,
@@ -580,35 +580,36 @@ exprt interpretert::get_value(
580
580
else if (real_type.id ()==ID_floatbv)
581
581
{
582
582
ieee_floatt f (to_floatbv_type (type));
583
- f.unpack (rhs[integer2size_t (offset)]);
583
+ f.unpack (rhs[numeric_cast_v<std:: size_t > (offset)]);
584
584
return f.to_expr ();
585
585
}
586
586
else if (real_type.id ()==ID_fixedbv)
587
587
{
588
588
fixedbvt f;
589
- f.from_integer (rhs[integer2size_t (offset)]);
589
+ f.from_integer (rhs[numeric_cast_v<std:: size_t > (offset)]);
590
590
return f.to_expr ();
591
591
}
592
592
else if (real_type.id ()==ID_bool)
593
593
{
594
- if (rhs[integer2size_t (offset)]!= 0 )
594
+ if (rhs[numeric_cast_v<std:: size_t > (offset)] != 0 )
595
595
return true_exprt ();
596
596
else
597
597
false_exprt ();
598
598
}
599
599
else if (real_type.id ()==ID_c_bool)
600
600
{
601
- return from_integer (rhs[integer2size_t (offset)]!=0 ?1 :0 , type);
601
+ return from_integer (
602
+ rhs[numeric_cast_v<std::size_t >(offset)] != 0 ? 1 : 0 , type);
602
603
}
603
604
else if (real_type.id () == ID_pointer)
604
605
{
605
- if (rhs[integer2size_t (offset)]== 0 )
606
+ if (rhs[numeric_cast_v<std:: size_t > (offset)] == 0 )
606
607
return null_pointer_exprt (to_pointer_type (real_type)); // NULL pointer
607
608
608
- if (rhs[integer2size_t (offset)]< memory.size ())
609
+ if (rhs[numeric_cast_v<std:: size_t > (offset)] < memory.size ())
609
610
{
610
611
// We want the symbol pointed to
611
- mp_integer address= rhs[integer2size_t (offset)];
612
+ mp_integer address = rhs[numeric_cast_v<std:: size_t > (offset)];
612
613
irep_idt identifier=address_to_identifier (address);
613
614
mp_integer offset=address_to_offset (address);
614
615
const typet type=get_type (identifier);
@@ -631,16 +632,18 @@ exprt interpretert::get_value(
631
632
return index_expr;
632
633
}
633
634
634
- error () << " interpreter: invalid pointer " << rhs[integer2size_t (offset)]
635
- << " > object count " << memory.size () << eom;
635
+ error () << " interpreter: invalid pointer "
636
+ << rhs[numeric_cast_v<std::size_t >(offset)] << " > object count "
637
+ << memory.size () << eom;
636
638
637
639
throw " interpreter: reading from invalid pointer" ;
638
640
}
639
641
else if (real_type.id ()==ID_string)
640
642
{
641
643
// Strings are currently encoded by their irep_idt ID.
642
644
return constant_exprt (
643
- get_string_container ().get_string (rhs[integer2size_t (offset)].to_long ()),
645
+ get_string_container ().get_string (
646
+ numeric_cast_v<std::size_t >(rhs[numeric_cast_v<std::size_t >(offset)])),
644
647
type);
645
648
}
646
649
@@ -680,8 +683,8 @@ void interpretert::execute_assign()
680
683
side_effect_exprt side_effect=to_side_effect_expr (code_assign.rhs ());
681
684
if (side_effect.get_statement ()==ID_nondet)
682
685
{
683
- mp_integer address=
684
- integer2size_t (evaluate_address (code_assign.lhs ()));
686
+ mp_integer address =
687
+ numeric_cast_v<std:: size_t > (evaluate_address (code_assign.lhs ()));
685
688
686
689
mp_integer size=
687
690
get_size (code_assign.lhs ().type ());
@@ -710,11 +713,11 @@ void interpretert::assign(
710
713
{
711
714
status () << total_steps << " ** assigning "
712
715
<< address_to_identifier (address_val) << " ["
713
- << address_to_offset (address_val) << " ]:= "
714
- << rhs[integer2size_t (i)]
715
- << " \n " << eom;
716
+ << address_to_offset (address_val)
717
+ << " ]:= " << rhs[numeric_cast_v<std:: size_t > (i)] << " \n "
718
+ << eom;
716
719
}
717
- cell.value = rhs[integer2size_t (i)];
720
+ cell.value = rhs[numeric_cast_v<std:: size_t > (i)];
718
721
if (cell.initialized ==memory_cellt::initializedt::UNKNOWN)
719
722
cell.initialized =memory_cellt::initializedt::WRITTEN_BEFORE_READ;
720
723
}
0 commit comments