Skip to content
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.

Sign up for GitHub

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

Jump to bottom

forall statement ensures clauses are missing well-formedness checks #2605

Closed
RustanLeino opened this issue Aug 17, 2022 · 0 comments · Fixed by #2606
Closed

forall statement ensures clauses are missing well-formedness checks #2605

RustanLeino opened this issue Aug 17, 2022 · 0 comments · Fixed by #2606
Assignees
@RustanLeino
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: verifier Translation from Dafny to Boogie (translator)

Comments

@RustanLeino
Copy link
Collaborator

The expression in the ensures clause of the following forall statement is not well-formed:

method M() {
  forall n | 0 <= n < 100
    ensures n / 0 == n / 0
  {
  }
}

Alas, this well-formedness check is missing, so Dafny currently accepts (and verifies) the method above.
@RustanLeino RustanLeino added kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: verifier Translation from Dafny to Boogie (translator) labels Aug 17, 2022
@RustanLeino RustanLeino self-assigned this Aug 17, 2022
RustanLeino added a commit to RustanLeino/dafny that referenced this issue Aug 17, 2022
@RustanLeino
fix: Check well-definedness of forall-ensures
2dae005 
Fixes dafny-lang#2605
@RustanLeino RustanLeino mentioned this issue Aug 17, 2022
Merged
keyboardDrummer pushed a commit that referenced this issue Aug 19, 2022
@RustanLeino
fix: Check well-definedness of forall-ensures (#2606)
cea5f12 
This PR adds the previously omitted well-definedness checks for the ensures clauses of forall statements.

Fixes #2605
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@RustanLeino RustanLeino

Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: verifier Translation from Dafny to Boogie (translator)
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

fix: Check well-definedness of forall-ensures RustanLeino/dafny
1 participant
@RustanLeino