-
Notifications
You must be signed in to change notification settings - Fork 48
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Inconsistent positions for postcondition #1480
Comments
This does not seem like a huge problem to me. In the end, the user may want to see the verification condition. But I was not aware that we write "INVALID" only on the error position line. This may be making the issue more sensitive. In reality, the definitions and paths also affect the validity. I get, for example the report (with --no-colors, but the issue is same anyway):
Should this not be printed as:
Namely, only the |
The following snippet:
gives the following position for the VC:
which seems to say that
y
is responsible for the invalidity but is just an artifact of the postcondition position.If however we use
val
s, we have:which is meaningful.
On the other hand, we do not use
StaticChecks.ensuring
(whether we usevar
orval
), we get:so we get 3 different positions for small tweaks. If we can at least rule out 1, that would be great. If we can make it consistent, that would be even better (we should however choose between option 2 and 3, I'd say 2 is more consistent because this is the positions we get in presence of branches).
The text was updated successfully, but these errors were encountered: