diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index c5ee73d76bd..b8216d9b163 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -1728,6 +1728,52 @@ std::string expr2ct::convert_object_descriptor( return result; } +static optionalt +build_sizeof_expr(const constant_exprt &expr, const namespacet &ns) +{ + const typet &type = static_cast(expr.find(ID_C_c_sizeof_type)); + + if(type.is_nil()) + return {}; + + const auto type_size_expr = size_of_expr(type, ns); + optionalt type_size; + if(type_size_expr.has_value()) + type_size = numeric_cast(*type_size_expr); + auto val = numeric_cast(expr); + + if( + !type_size.has_value() || *type_size < 0 || !val.has_value() || + *val < *type_size || (*type_size == 0 && *val > 0)) + { + return {}; + } + + const unsignedbv_typet t(size_type()); + DATA_INVARIANT( + address_bits(*val + 1) <= t.get_width(), + "sizeof value does not fit size_type"); + + mp_integer remainder = 0; + + if(*type_size != 0) + { + remainder = *val % *type_size; + *val -= remainder; + *val /= *type_size; + } + + exprt result(ID_sizeof, t); + result.set(ID_type_arg, type); + + if(*val > 1) + result = mult_exprt(result, from_integer(*val, t)); + if(remainder > 0) + result = plus_exprt(result, from_integer(remainder, t)); + + return typecast_exprt::conditional_cast(result, expr.type()); +} + std::string expr2ct::convert_constant( const constant_exprt &src, unsigned &precedence) @@ -1852,11 +1898,9 @@ std::string expr2ct::convert_constant( else if(c_type==ID_signed_long_long_int) dest+="ll"; - if(src.find(ID_C_c_sizeof_type).is_not_nil() && - sizeof_nesting==0) + if(sizeof_nesting == 0) { - const auto sizeof_expr_opt = - build_sizeof_expr(to_constant_expr(src), ns); + const auto sizeof_expr_opt = build_sizeof_expr(src, ns); if(sizeof_expr_opt.has_value()) { diff --git a/src/util/pointer_offset_size.cpp b/src/util/pointer_offset_size.cpp index 246fbecc3e6..23b688eea44 100644 --- a/src/util/pointer_offset_size.cpp +++ b/src/util/pointer_offset_size.cpp @@ -560,50 +560,6 @@ compute_pointer_offset(const exprt &expr, const namespacet &ns) return {}; // don't know } -optionalt -build_sizeof_expr(const constant_exprt &expr, const namespacet &ns) -{ - const typet &type= - static_cast(expr.find(ID_C_c_sizeof_type)); - - if(type.is_nil()) - return {}; - - const auto type_size = pointer_offset_size(type, ns); - auto val = numeric_cast(expr); - - if( - !type_size.has_value() || *type_size < 0 || !val.has_value() || - *val < *type_size || (*type_size == 0 && *val > 0)) - { - return {}; - } - - const typet t(size_type()); - DATA_INVARIANT( - address_bits(*val + 1) <= *pointer_offset_bits(t, ns), - "sizeof value does not fit size_type"); - - mp_integer remainder=0; - - if(*type_size != 0) - { - remainder = *val % *type_size; - *val -= remainder; - *val /= *type_size; - } - - exprt result(ID_sizeof, t); - result.set(ID_type_arg, type); - - if(*val > 1) - result = mult_exprt(result, from_integer(*val, t)); - if(remainder>0) - result=plus_exprt(result, from_integer(remainder, t)); - - return typecast_exprt::conditional_cast(result, expr.type()); -} - optionalt get_subexpression_at_offset( const exprt &expr, const mp_integer &offset_bytes, diff --git a/src/util/pointer_offset_size.h b/src/util/pointer_offset_size.h index f75d0586c39..ac44ac92958 100644 --- a/src/util/pointer_offset_size.h +++ b/src/util/pointer_offset_size.h @@ -51,9 +51,6 @@ optionalt member_offset_expr( optionalt size_of_expr(const typet &type, const namespacet &ns); -optionalt -build_sizeof_expr(const constant_exprt &expr, const namespacet &ns); - optionalt get_subexpression_at_offset( const exprt &expr, const mp_integer &offset,