-
Notifications
You must be signed in to change notification settings - Fork 254
Issues: dafny-lang/dafny
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
Author
Label
Projects
Milestones
Assignee
Sort
Issues list
Cannot prove tautology with map, opaque function and transparent function.
has-workaround: yes
There is a known workaround
incompleteness
Things that Dafny should be able to prove, but can't
part: boogie
Happens after passing the program to Boogie
part: verifier
Translation from Dafny to Boogie (translator)
#2308
opened Jun 28, 2022 by
MikaelMayer
Can't prove modifies clause
area: error-reporting
Clarity of the error reporting
incompleteness
Things that Dafny should be able to prove, but can't
#3265
opened Dec 23, 2022 by
MikaelMayer
Having doo files part of the git index prevents agile development
area: build-system
Support for dependencies in Dafny, generation of target language build files
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#5057
opened Feb 6, 2024 by
MikaelMayer
this is not fresh and fresh in well-formedness
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
introduced: v4.1.0
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
makes-mikael-grateful
This issue, is fixed, would make Mikael Mayer grateful
part: verifier
Translation from Dafny to Boogie (translator)
priority: next
Will consider working on this after in progress work is done
#4700
opened Oct 20, 2023 by
MikaelMayer
Unsound use of A bug in the Dafny compiler that causes a correct Dafny program to execute incorrectly
introduced: pre-2012
{this}
in constant initialization
during 4: bad execution of correct program
#2923
opened Oct 25, 2022 by
MikaelMayer
Flaky LSP test: DocumentAddedToExistingProjectDoesNotCrash
kind: language development speed
Slows down development of Dafny the language, flaky tests
part: language server
Support for LSP in Dafny (server part; client is in ide-vscode repo)
priority: next
Will consider working on this after in progress work is done
#5434
opened May 13, 2024 by
MikaelMayer
ProTip!
Exclude everything labeled
bug
with -label:bug.