Open peterwvj opened 7 years ago
The expression and/or statement finders need to be enhanced to "find" the expression body of the assignment definition (the dcl). Just fixing that may be enough to solve this issue.
I did attempt to fix this, but there is something complicated going on between definition, statement and expression based finder visitors and I couldn't easily see how to fix it. This example is awkward, because we have a statement block that contains a definition that contains an expression.
Overture will allow you to set a breakpoint on a
dcl
statement, likedcl x : nat := 123
. But in the command line, you're not allowed to do that - it says that there are no breakable expressions or statements on that line (although in principle there are).But the real problem is that if you debug a spec with a BP set on a
dcl
statement, you get errors or warnings in the log. You always get a warning, but you also sometimes get a fatal error.This issue can be demonstrated using the following model:
The stack traces you get look like: