Skip to content

Commit 673bd73

Browse files
committed
Cleanup build_sizeof_expr
Make sure we use any peculiar properties of "sizeof" that size_of_expr will make sure to handle: pointer_offset_size performs size computation using the runtime size, and not C-frontend specific oddities.
1 parent 85d99a4 commit 673bd73

File tree

1 file changed

+6
-3
lines changed

1 file changed

+6
-3
lines changed

src/ansi-c/expr2c.cpp

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1736,7 +1736,10 @@ build_sizeof_expr(const constant_exprt &expr, const namespacet &ns)
17361736
if(type.is_nil())
17371737
return {};
17381738

1739-
const auto type_size = pointer_offset_size(type, ns);
1739+
const auto type_size_expr = size_of_expr(type, ns);
1740+
optionalt<mp_integer> type_size;
1741+
if(type_size_expr.has_value())
1742+
type_size = numeric_cast<mp_integer>(*type_size_expr);
17401743
auto val = numeric_cast<mp_integer>(expr);
17411744

17421745
if(
@@ -1746,9 +1749,9 @@ build_sizeof_expr(const constant_exprt &expr, const namespacet &ns)
17461749
return {};
17471750
}
17481751

1749-
const typet t(size_type());
1752+
const unsignedbv_typet t(size_type());
17501753
DATA_INVARIANT(
1751-
address_bits(*val + 1) <= *pointer_offset_bits(t, ns),
1754+
address_bits(*val + 1) <= t.get_width(),
17521755
"sizeof value does not fit size_type");
17531756

17541757
mp_integer remainder = 0;

0 commit comments

Comments
 (0)