Skip to content

Commit fdbc233

Browse files
committed
Do not throw any exceptions in byte-operator lowering
The two remaining cases really _are_ invariants.
1 parent 1e8d38d commit fdbc233

File tree

1 file changed

+9
-10
lines changed

1 file changed

+9
-10
lines changed

src/solvers/lowering/byte_operators.cpp

Lines changed: 9 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -567,10 +567,10 @@ static array_exprt unpack_struct(
567567
// us with unknown alignment of subsequent members, and queuing them up as
568568
// bit fields is not possible either as the total width of the concatenation
569569
// could not be determined.
570-
if(
571-
!component_bits.has_value() &&
572-
(std::next(it) != components.end() || bit_fields.has_value()))
573-
throw non_constant_widtht(src, nil_exprt());
570+
DATA_INVARIANT(
571+
component_bits.has_value() ||
572+
(std::next(it) == components.end() && !bit_fields.has_value()),
573+
"members of non-constant width should come last in a struct");
574574

575575
member_exprt member(src, comp.get_name(), comp.type());
576576
if(src.id() == ID_struct)
@@ -1173,12 +1173,11 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
11731173
if(!size_bits.has_value())
11741174
{
11751175
auto op0_bits = pointer_offset_bits(unpacked.op().type(), ns);
1176-
if(!op0_bits.has_value())
1177-
{
1178-
throw non_const_byte_extraction_sizet(unpacked);
1179-
}
1180-
else
1181-
size_bits=op0_bits;
1176+
// all cases with non-constant width should have been handled above
1177+
DATA_INVARIANT(
1178+
op0_bits.has_value(),
1179+
"the extracted width or the source width must be known");
1180+
size_bits = op0_bits;
11821181
}
11831182

11841183
mp_integer num_elements =

0 commit comments

Comments
 (0)