Broken support for `address_of(labelt)` in incremental smt2 decision procedure.
Opened this issue · 0 comments
esteffin commented
In the incremental smt2 decision procedure the find_object_base_expression
function has a case for code_labelt
, however the template specialization function can_cast_expr<code_labelt>
requires the code_labelt
to be inside a codet
block.
This, other than being counter-intuitive as per expected semantics of the can_cast_expr
function, fails to cast the argument of address_of
to code_labelt
when not in a codet
.
This causes a failure with invariant Unable to find base object of expression: label
in find_object_base_expression
.
This is required for the following test:
- cbmc/Computed-Goto1/test.desc