Skip to content

Commit 85d99a4

Browse files
committed
Move build_sizeof_expr to expr2c
expr2c is the only user of a function that does entirely C-frontend-specific work. It constructs a "sizeof" expression in the way the C frontend expects such an expression to look like.
1 parent e831f43 commit 85d99a4

File tree

3 files changed

+45
-51
lines changed

3 files changed

+45
-51
lines changed

src/ansi-c/expr2c.cpp

Lines changed: 45 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1728,6 +1728,49 @@ std::string expr2ct::convert_object_descriptor(
17281728
return result;
17291729
}
17301730

1731+
static optionalt<exprt>
1732+
build_sizeof_expr(const constant_exprt &expr, const namespacet &ns)
1733+
{
1734+
const typet &type = static_cast<const typet &>(expr.find(ID_C_c_sizeof_type));
1735+
1736+
if(type.is_nil())
1737+
return {};
1738+
1739+
const auto type_size = pointer_offset_size(type, ns);
1740+
auto val = numeric_cast<mp_integer>(expr);
1741+
1742+
if(
1743+
!type_size.has_value() || *type_size < 0 || !val.has_value() ||
1744+
*val < *type_size || (*type_size == 0 && *val > 0))
1745+
{
1746+
return {};
1747+
}
1748+
1749+
const typet t(size_type());
1750+
DATA_INVARIANT(
1751+
address_bits(*val + 1) <= *pointer_offset_bits(t, ns),
1752+
"sizeof value does not fit size_type");
1753+
1754+
mp_integer remainder = 0;
1755+
1756+
if(*type_size != 0)
1757+
{
1758+
remainder = *val % *type_size;
1759+
*val -= remainder;
1760+
*val /= *type_size;
1761+
}
1762+
1763+
exprt result(ID_sizeof, t);
1764+
result.set(ID_type_arg, type);
1765+
1766+
if(*val > 1)
1767+
result = mult_exprt(result, from_integer(*val, t));
1768+
if(remainder > 0)
1769+
result = plus_exprt(result, from_integer(remainder, t));
1770+
1771+
return typecast_exprt::conditional_cast(result, expr.type());
1772+
}
1773+
17311774
std::string expr2ct::convert_constant(
17321775
const constant_exprt &src,
17331776
unsigned &precedence)
@@ -1852,11 +1895,9 @@ std::string expr2ct::convert_constant(
18521895
else if(c_type==ID_signed_long_long_int)
18531896
dest+="ll";
18541897

1855-
if(src.find(ID_C_c_sizeof_type).is_not_nil() &&
1856-
sizeof_nesting==0)
1898+
if(sizeof_nesting == 0)
18571899
{
1858-
const auto sizeof_expr_opt =
1859-
build_sizeof_expr(to_constant_expr(src), ns);
1900+
const auto sizeof_expr_opt = build_sizeof_expr(src, ns);
18601901

18611902
if(sizeof_expr_opt.has_value())
18621903
{

src/util/pointer_offset_size.cpp

Lines changed: 0 additions & 44 deletions
Original file line numberDiff line numberDiff line change
@@ -560,50 +560,6 @@ compute_pointer_offset(const exprt &expr, const namespacet &ns)
560560
return {}; // don't know
561561
}
562562

563-
optionalt<exprt>
564-
build_sizeof_expr(const constant_exprt &expr, const namespacet &ns)
565-
{
566-
const typet &type=
567-
static_cast<const typet &>(expr.find(ID_C_c_sizeof_type));
568-
569-
if(type.is_nil())
570-
return {};
571-
572-
const auto type_size = pointer_offset_size(type, ns);
573-
auto val = numeric_cast<mp_integer>(expr);
574-
575-
if(
576-
!type_size.has_value() || *type_size < 0 || !val.has_value() ||
577-
*val < *type_size || (*type_size == 0 && *val > 0))
578-
{
579-
return {};
580-
}
581-
582-
const typet t(size_type());
583-
DATA_INVARIANT(
584-
address_bits(*val + 1) <= *pointer_offset_bits(t, ns),
585-
"sizeof value does not fit size_type");
586-
587-
mp_integer remainder=0;
588-
589-
if(*type_size != 0)
590-
{
591-
remainder = *val % *type_size;
592-
*val -= remainder;
593-
*val /= *type_size;
594-
}
595-
596-
exprt result(ID_sizeof, t);
597-
result.set(ID_type_arg, type);
598-
599-
if(*val > 1)
600-
result = mult_exprt(result, from_integer(*val, t));
601-
if(remainder>0)
602-
result=plus_exprt(result, from_integer(remainder, t));
603-
604-
return typecast_exprt::conditional_cast(result, expr.type());
605-
}
606-
607563
optionalt<exprt> get_subexpression_at_offset(
608564
const exprt &expr,
609565
const mp_integer &offset_bytes,

src/util/pointer_offset_size.h

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -51,9 +51,6 @@ optionalt<exprt> member_offset_expr(
5151

5252
optionalt<exprt> size_of_expr(const typet &type, const namespacet &ns);
5353

54-
optionalt<exprt>
55-
build_sizeof_expr(const constant_exprt &expr, const namespacet &ns);
56-
5754
optionalt<exprt> get_subexpression_at_offset(
5855
const exprt &expr,
5956
const mp_integer &offset,

0 commit comments

Comments
 (0)