@@ -1072,7 +1072,7 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
1072
1072
src.id () == ID_byte_extract_big_endian);
1073
1073
const bool little_endian = src.id () == ID_byte_extract_little_endian;
1074
1074
1075
- // determine an upper bound of the number of bytes we might need
1075
+ // determine an upper bound of the last byte we might need
1076
1076
auto upper_bound_opt = size_of_expr (src.type (), ns);
1077
1077
if (upper_bound_opt.has_value ())
1078
1078
{
@@ -1106,6 +1106,7 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
1106
1106
if (element_bits.has_value () && *element_bits >= 1 && *element_bits % 8 == 0 )
1107
1107
{
1108
1108
auto num_elements = numeric_cast<std::size_t >(array_type.size ());
1109
+ // XXX: This can't be right -- unpacked is a byte array, whereas array_type may have larger elements
1109
1110
if (!num_elements.has_value () && unpacked.op ().id () == ID_array)
1110
1111
num_elements = unpacked.op ().operands ().size ();
1111
1112
@@ -1286,11 +1287,10 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
1286
1287
size_bits = op0_bits;
1287
1288
}
1288
1289
1289
- mp_integer num_elements =
1290
- (*size_bits) / 8 + (((*size_bits) % 8 == 0 ) ? 0 : 1 );
1290
+ mp_integer num_bytes = (*size_bits) / 8 + (((*size_bits) % 8 == 0 ) ? 0 : 1 );
1291
1291
1292
1292
// get 'width'-many bytes, and concatenate
1293
- const std::size_t width_bytes = numeric_cast_v<std::size_t >(num_elements );
1293
+ const std::size_t width_bytes = numeric_cast_v<std::size_t >(num_bytes );
1294
1294
exprt::operandst op;
1295
1295
op.reserve (width_bytes);
1296
1296
0 commit comments