Open
Description
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.