Skip to content

Filter fewer synthetic locations for abstract debugger #1336

Open
@sim642

Description

@sim642

Currently the abstract debugger uses the same ARG and CFG-location mappings as witnesses, including the same notion of synthetic locations. However, this is not ideal for abstract debugging, where too many nodes are excluded as synthetic.

For example, placing a breakpoint on line 1 (where the loop head is synthetic) finds a node inside the loop instead:

while (cond) {
   ...
}

This is probably even worse with for loops, where many intermediate locations are possible (and separate in CFG). For abstract debugging it'd be nice to allow those locations since they don't have to be valid for insertion of assert statements, but just lookup of loop head nodes, etc.

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