@@ -477,24 +477,28 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
477
477
std::cout << "O: " << format(root_object) << '\n';
478
478
#endif
479
479
480
- valuet result;
481
-
482
480
if (root_object.id () == ID_null_object)
483
481
{
484
- if (o.offset ().is_zero ())
485
- result.pointer = null_pointer_exprt{pointer_type};
486
- else
487
- return valuet{};
482
+ if (!o.offset ().is_zero ())
483
+ return {};
484
+
485
+ valuet result;
486
+ result.pointer = null_pointer_exprt{pointer_type};
487
+ return result;
488
488
}
489
489
else if (root_object.id ()==ID_dynamic_object)
490
490
{
491
+ valuet result;
492
+
491
493
// constraint that it actually is a dynamic object
492
494
// this is also our guard
493
495
result.pointer_guard = is_dynamic_object_exprt (pointer_expr);
494
496
495
497
// can't remove here, turn into *p
496
498
result.value = dereference_exprt{pointer_expr};
497
499
result.pointer = pointer_expr;
500
+
501
+ return result;
498
502
}
499
503
else if (root_object.id ()==ID_integer_address)
500
504
{
@@ -514,8 +518,10 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
514
518
pointer_offset (pointer_expr),
515
519
to_array_type (memory_symbol.type ).element_type ());
516
520
521
+ valuet result;
517
522
result.value =index_expr;
518
523
result.pointer = address_of_exprt{index_expr};
524
+ return result;
519
525
}
520
526
else if (dereference_type_compare (
521
527
to_array_type (memory_symbol.type ).element_type (),
@@ -526,28 +532,32 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
526
532
symbol_expr,
527
533
pointer_offset (pointer_expr),
528
534
to_array_type (memory_symbol.type ).element_type ());
535
+
536
+ valuet result;
529
537
result.value =typecast_exprt (index_expr, dereference_type);
530
538
result.pointer =
531
539
typecast_exprt{address_of_exprt{index_expr}, pointer_type};
540
+ return result;
532
541
}
533
542
else
534
543
{
535
544
// We need to use byte_extract.
536
545
// Won't do this without a commitment to an endianness.
537
546
538
547
if (config.ansi_c .endianness ==configt::ansi_ct::endiannesst::NO_ENDIANNESS)
539
- {
540
- }
541
- else
542
- {
543
- result.value = make_byte_extract (
544
- symbol_expr, pointer_offset (pointer_expr), dereference_type);
545
- result.pointer = address_of_exprt{result.value };
546
- }
548
+ return {};
549
+
550
+ valuet result;
551
+ result.value = make_byte_extract (
552
+ symbol_expr, pointer_offset (pointer_expr), dereference_type);
553
+ result.pointer = address_of_exprt{result.value };
554
+ return result;
547
555
}
548
556
}
549
557
else
550
558
{
559
+ valuet result;
560
+
551
561
// something generic -- really has to be a symbol
552
562
address_of_exprt object_pointer (object);
553
563
@@ -651,17 +661,11 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
651
661
result.pointer = typecast_exprt::conditional_cast (
652
662
address_of_exprt{skip_typecast (o.root_object ())}, pointer_type);
653
663
654
- if (memory_model (result.value , dereference_type, offset, ns))
655
- {
656
- // ok, done
657
- }
658
- else
659
- {
660
- return valuet (); // give up, no way that this is ok
661
- }
662
- }
664
+ if (!memory_model (result.value , dereference_type, offset, ns))
665
+ return {}; // give up, no way that this is ok
663
666
664
- return result;
667
+ return result;
668
+ }
665
669
}
666
670
667
671
static bool is_a_bv_type (const typet &type)
0 commit comments