Skip to content

Commit 6633948

Browse files
committed
Pointer dereferencing: code cleanup in build_reference_to
Avoid starting with an uninitialised expression, instead declare it at the point of definition.
1 parent e64675a commit 6633948

File tree

1 file changed

+3
-13
lines changed

1 file changed

+3
-13
lines changed

src/pointer-analysis/value_set_dereference.cpp

Lines changed: 3 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -595,8 +595,6 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
595595
else
596596
offset=pointer_offset(pointer_expr);
597597

598-
exprt adjusted_offset;
599-
600598
// are we doing a byte?
601599
auto element_size =
602600
pointer_offset_size(to_array_type(root_object_type).element_type(), ns);
@@ -606,19 +604,11 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
606604
throw "unknown or invalid type size of:\n" +
607605
to_array_type(root_object_type).element_type().pretty();
608606
}
609-
else if(*element_size == 1)
610-
{
611-
// no need to adjust offset
612-
adjusted_offset = offset;
613-
}
614-
else
615-
{
616-
exprt element_size_expr = from_integer(*element_size, offset.type());
617607

618-
adjusted_offset=binary_exprt(
619-
offset, ID_div, element_size_expr, offset.type());
608+
exprt element_size_expr = from_integer(*element_size, offset.type());
620609

621-
}
610+
exprt adjusted_offset =
611+
simplify_expr(div_exprt{offset, element_size_expr}, ns);
622612

623613
index_exprt index_expr{root_object, adjusted_offset};
624614
result.value =

0 commit comments

Comments
 (0)