Skip to content

Commit 18ac0b4

Browse files
committed
Unit test lower_byte_update of/from an array of bits
Byte operator lowering made several assumptions about array elements being byte aligned, which may be true for ANSI C, but isn't the case for our C front-end (which supports arrays of single bits), and not true for the overall framework in general.
1 parent bd41e25 commit 18ac0b4

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

unit/solvers/lowering/byte_operators.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -429,6 +429,7 @@ SCENARIO("byte_update_lowering", "[core][solvers][lowering][byte_update]")
429429
union_typet({{"compA", u32}, {"compB", u64}}),
430430
c_enum_typet(u16),
431431
c_enum_typet(unsignedbv_typet(128)),
432+
array_typet{bv_typet{1}, from_integer(128, size_type())},
432433
array_typet(u8, size),
433434
array_typet(s32, size),
434435
array_typet(u64, size),

0 commit comments

Comments
 (0)