diffblue/cbmc

Broken support for `address_of(labelt)` in incremental smt2 decision procedure.

Opened this issue · 0 comments

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