@@ -424,11 +424,11 @@ void interpretert::execute_decl()
424
424
struct_typet::componentt
425
425
interpretert::get_component (const typet &object_type, const mp_integer &offset)
426
426
{
427
- const typet real_type = ns.follow (object_type);
428
- if (real_type.id ()!=ID_struct)
427
+ if (object_type.id () != ID_struct_tag)
429
428
throw " request for member of non-struct" ;
430
429
431
- const struct_typet &struct_type=to_struct_type (real_type);
430
+ const struct_typet &struct_type =
431
+ ns.follow_tag (to_struct_tag_type (object_type));
432
432
const struct_typet::componentst &components=struct_type.components ();
433
433
434
434
mp_integer tmp_offset=offset;
@@ -460,11 +460,10 @@ exprt interpretert::get_value(
460
460
const mp_integer &offset,
461
461
bool use_non_det)
462
462
{
463
- const typet real_type=ns.follow (type);
464
- if (real_type.id ()==ID_struct)
463
+ if (type.id () == ID_struct_tag)
465
464
{
466
- struct_exprt result ({}, real_type );
467
- const struct_typet &struct_type= to_struct_type (real_type );
465
+ struct_exprt result ({}, type );
466
+ const struct_typet &struct_type = ns. follow_tag ( to_struct_tag_type (type) );
468
467
const struct_typet::componentst &components=struct_type.components ();
469
468
470
469
// Retrieve the values for the individual members
@@ -482,10 +481,10 @@ exprt interpretert::get_value(
482
481
483
482
return std::move (result);
484
483
}
485
- else if (real_type .id ()== ID_array)
484
+ else if (type .id () == ID_array)
486
485
{
487
486
// Get size of array
488
- array_exprt result ({}, to_array_type (real_type ));
487
+ array_exprt result ({}, to_array_type (type ));
489
488
const exprt &size_expr = to_array_type (type).size ();
490
489
mp_integer subtype_size = get_size (to_array_type (type).element_type ());
491
490
mp_integer count;
@@ -526,13 +525,12 @@ exprt interpretert::get_value(
526
525
mp_vectort &rhs,
527
526
const mp_integer &offset)
528
527
{
529
- const typet real_type=ns.follow (type);
530
528
PRECONDITION (!rhs.empty ());
531
529
532
- if (real_type .id ()==ID_struct )
530
+ if (type .id () == ID_struct_tag )
533
531
{
534
- struct_exprt result ({}, real_type );
535
- const struct_typet &struct_type= to_struct_type (real_type );
532
+ struct_exprt result ({}, type );
533
+ const struct_typet &struct_type = ns. follow_tag ( to_struct_tag_type (type) );
536
534
const struct_typet::componentst &components=struct_type.components ();
537
535
538
536
// Retrieve the values for the individual members
@@ -548,10 +546,10 @@ exprt interpretert::get_value(
548
546
}
549
547
return std::move (result);
550
548
}
551
- else if (real_type .id ()== ID_array)
549
+ else if (type .id () == ID_array)
552
550
{
553
- array_exprt result ({}, to_array_type (real_type ));
554
- const exprt &size_expr = to_array_type (real_type ).size ();
551
+ array_exprt result ({}, to_array_type (type ));
552
+ const exprt &size_expr = to_array_type (type ).size ();
555
553
556
554
// Get size of array
557
555
mp_integer subtype_size = get_size (to_array_type (type).element_type ());
@@ -576,34 +574,34 @@ exprt interpretert::get_value(
576
574
}
577
575
return std::move (result);
578
576
}
579
- else if (real_type .id ()== ID_floatbv)
577
+ else if (type .id () == ID_floatbv)
580
578
{
581
579
ieee_floatt f (to_floatbv_type (type));
582
580
f.unpack (rhs[numeric_cast_v<std::size_t >(offset)]);
583
581
return f.to_expr ();
584
582
}
585
- else if (real_type .id ()== ID_fixedbv)
583
+ else if (type .id () == ID_fixedbv)
586
584
{
587
585
fixedbvt f;
588
586
f.from_integer (rhs[numeric_cast_v<std::size_t >(offset)]);
589
587
return f.to_expr ();
590
588
}
591
- else if (real_type .id ()== ID_bool)
589
+ else if (type .id () == ID_bool)
592
590
{
593
591
if (rhs[numeric_cast_v<std::size_t >(offset)] != 0 )
594
592
return true_exprt ();
595
593
else
596
594
false_exprt ();
597
595
}
598
- else if (real_type .id ()== ID_c_bool)
596
+ else if (type .id () == ID_c_bool)
599
597
{
600
598
return from_integer (
601
599
rhs[numeric_cast_v<std::size_t >(offset)] != 0 ? 1 : 0 , type);
602
600
}
603
- else if (real_type .id () == ID_pointer)
601
+ else if (type .id () == ID_pointer)
604
602
{
605
603
if (rhs[numeric_cast_v<std::size_t >(offset)] == 0 )
606
- return null_pointer_exprt (to_pointer_type (real_type )); // NULL pointer
604
+ return null_pointer_exprt (to_pointer_type (type )); // NULL pointer
607
605
608
606
if (rhs[numeric_cast_v<std::size_t >(offset)] < memory.size ())
609
607
{
@@ -634,7 +632,7 @@ exprt interpretert::get_value(
634
632
635
633
throw " interpreter: reading from invalid pointer" ;
636
634
}
637
- else if (real_type .id ()== ID_string)
635
+ else if (type .id () == ID_string)
638
636
{
639
637
// Strings are currently encoded by their irep_idt ID.
640
638
return constant_exprt (
0 commit comments