Commit 7118b73
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: #83031 parent 37511f3 commit 7118b73
1 file changed
+4
-3
lines changed| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
346 | 346 | | |
347 | 347 | | |
348 | 348 | | |
349 | | - | |
| 349 | + | |
| 350 | + | |
| 351 | + | |
350 | 352 | | |
351 | 353 | | |
352 | 354 | | |
353 | 355 | | |
354 | | - | |
355 | | - | |
| 356 | + | |
356 | 357 | | |
357 | 358 | | |
358 | 359 | | |
| |||
0 commit comments