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

Replace Translator.assertionCount by something more reliable. #3251

Open
keyboardDrummer opened this issue Dec 22, 2022 · 2 comments
Open

Replace Translator.assertionCount by something more reliable. #3251

keyboardDrummer opened this issue Dec 22, 2022 · 2 comments
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: verifier Translation from Dafny to Boogie (translator)

Comments

@keyboardDrummer
Copy link
Member

Our code has a mechanism that when used incorrectly produces soundness bugs, and could be replaced by something reliable. More context in the discussion here: #3244
@keyboardDrummer keyboardDrummer added kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: verifier Translation from Dafny to Boogie (translator) during 3: execution of incorrect program An bug in the verifier that allows Dafny to run a program that does not correctly implement its spec labels Dec 22, 2022
@cpitclaudel
Copy link
Member

Is it OK to remove the severity: soundness flag from this? We usually use that only for bugs that let you prove false, not for design issues that are likely to lead to soundness bugs.

(I'll do so for now, please feel free to revert). I won't touch the "bug" classification, even though I would have used "enhancement" myself.

@cpitclaudel cpitclaudel removed the during 3: execution of incorrect program An bug in the verifier that allows Dafny to run a program that does not correctly implement its spec label Dec 23, 2022
@keyboardDrummer
Copy link
Member Author

Is it OK to remove the severity: soundness flag from this? We usually use that only for bugs that let you prove false, not for design issues that are likely to lead to soundness bugs.

OK with me, but there might be an undiscovered soundness bug here.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
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

No branches or pull requests
2 participants
@keyboardDrummer @cpitclaudel