Skip to content

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

Open
@esteffin

Description

@esteffin

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

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions