From 3008132a2eeee3c3a782c8ba342c5c96aea6df41 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 29 Nov 2021 14:20:58 +0000 Subject: [PATCH] Byte operator lowering: additional preconditions in instantiate_byte_array No code changes, just additional safety checks to guard against implementation errors: instantiate_byte_array requires a byte array or vector typed source operand. Other kinds of arrays/vectors are not supported or expected. --- src/solvers/lowering/byte_operators.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/solvers/lowering/byte_operators.cpp b/src/solvers/lowering/byte_operators.cpp index fad23110da8..7d5c21fe23b 100644 --- a/src/solvers/lowering/byte_operators.cpp +++ b/src/solvers/lowering/byte_operators.cpp @@ -405,6 +405,10 @@ static exprt::operandst instantiate_byte_array( src.operands().begin() + narrow_cast(upper_bound)}; } + PRECONDITION(src.type().id() == ID_array || src.type().id() == ID_vector); + PRECONDITION( + can_cast_type(src.type().subtype()) && + to_bitvector_type(src.type().subtype()).get_width() == 8); exprt::operandst bytes; bytes.reserve(upper_bound - lower_bound); for(std::size_t i = lower_bound; i < upper_bound; ++i)