From 7118b73733a47e6843342dda4349479a304c4373 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 10 Jun 2024 10:36:42 +0000 Subject: [PATCH] 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 --- src/util/lower_byte_operators.cpp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/util/lower_byte_operators.cpp b/src/util/lower_byte_operators.cpp index 5b585cbd98c..889f851fc2c 100644 --- a/src/util/lower_byte_operators.cpp +++ b/src/util/lower_byte_operators.cpp @@ -346,13 +346,14 @@ static exprt bv_to_expr( else if( can_cast_type(target_type) || target_type.id() == ID_c_enum || target_type.id() == ID_c_enum_tag || - target_type.id() == ID_string) + target_type.id() == ID_string || + (target_type.id() == ID_bool && + to_bitvector_type(bitvector_expr.type()).get_width() == 1)) { return simplify_expr( typecast_exprt::conditional_cast(bitvector_expr, target_type), ns); } - - if(target_type.id() == ID_struct) + else if(target_type.id() == ID_struct) { return bv_to_struct_expr( bitvector_expr, to_struct_type(target_type), endianness_map, ns);