Skip to content

Commit 7118b73

Browse files
committed
Lower-byte-operators: bv_to_expr should support bool target type
When byte updating or byte extracting structs that contain single-bit `__CPROVER_bool` members (as is used in `__CPROVER_contracts_car_t`) we may need to turn a `bv` typed single-bit `extractbits` expression into one that has `bool` (`__CPROVER_bool`) type. Fixes: #8303
1 parent 37511f3 commit 7118b73

File tree

1 file changed

+4
-3
lines changed

1 file changed

+4
-3
lines changed

src/util/lower_byte_operators.cpp

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -346,13 +346,14 @@ static exprt bv_to_expr(
346346
else if(
347347
can_cast_type<bitvector_typet>(target_type) ||
348348
target_type.id() == ID_c_enum || target_type.id() == ID_c_enum_tag ||
349-
target_type.id() == ID_string)
349+
target_type.id() == ID_string ||
350+
(target_type.id() == ID_bool &&
351+
to_bitvector_type(bitvector_expr.type()).get_width() == 1))
350352
{
351353
return simplify_expr(
352354
typecast_exprt::conditional_cast(bitvector_expr, target_type), ns);
353355
}
354-
355-
if(target_type.id() == ID_struct)
356+
else if(target_type.id() == ID_struct)
356357
{
357358
return bv_to_struct_expr(
358359
bitvector_expr, to_struct_type(target_type), endianness_map, ns);

0 commit comments

Comments
 (0)