Skip to content

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.

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

Clear current search query, filters, and sorts
1,046 Open 1,614 Closed
1,046 Open 1,614 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

Using --default-function-opacity=AutoRevealDependencies can perform badly during 2: compilation of correct program Dafny rejects a valid program during compilation kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: verifier Translation from Dafny to Boogie (translator) priority: not yet Will reconsider working on this when we're looking for work
#5272 opened Mar 28, 2024 by atomb
Allow using project files together with --library 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
#5336 opened Apr 19, 2024 by keyboardDrummer
1
Enable safely using doo files that were verified against other doo files 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 kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label priority: not yet Will reconsider working on this when we're looking for work
#5335 opened Apr 19, 2024 by keyboardDrummer
4
Compilation to not use a global local variable counter, but a local one kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny priority: next Will consider working on this after in progress work is done
#5330 opened Apr 17, 2024 by MikaelMayer
1
2
Holistic design for Dafny package management kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny status: planned The team is planning to work on this in the near future
#5323 opened Apr 16, 2024 by robin-aws Library support
@robin-aws
Unstable test due to timeout when executing Rust back-end kind: language development speed Slows down development of Dafny the language, flaky tests priority: next Will consider working on this after in progress work is done
#5321 opened Apr 15, 2024 by keyboardDrummer
1
Unstable test 'VerificationDiagnosticsCanBeMigratedAcrossMultipleResolutions kind: language development speed Slows down development of Dafny the language, flaky tests priority: next Will consider working on this after in progress work is done
#5319 opened Apr 12, 2024 by keyboardDrummer
@keyboardDrummer
1
When running many iterations, they get progressively slower until one gets stuck during 1: program development Bad error message or documentation; IDE bug; crash compiling invalid program kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label priority: not yet Will reconsider working on this when we're looking for work
#5316 opened Apr 11, 2024 by hmijail
6
Unstable test QuickEditsInLargeFile kind: language development speed Slows down development of Dafny the language, flaky tests priority: next Will consider working on this after in progress work is done
#5304 opened Apr 5, 2024 by keyboardDrummer
@keyboardDrummer
1
Bitvectors using too much time/resources area: performance Performance issues kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: boogie Happens after passing the program to Boogie part: verifier Translation from Dafny to Boogie (translator)
#5298 opened Apr 4, 2024 by seanmcl
3
Refactor reading doo manifest from Backend to AST kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny kind: language development speed Slows down development of Dafny the language, flaky tests
#5296 opened Apr 4, 2024 by ShubhamChaturvedi7
Unstable VerificationErrorDetectedAfterCanceledSave kind: language development speed Slows down development of Dafny the language, flaky tests priority: next Will consider working on this after in progress work is done
#5292 opened Apr 3, 2024 by keyboardDrummer
@keyboardDrummer
1
Precondition of merge sort too strong during 2: compilation of correct program Dafny rejects a valid program during compilation kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: standard libraries Standard libraries packaged in the Dafny distribution priority: next Will consider working on this after in progress work is done
#5286 opened Apr 1, 2024 by RustanLeino
@robin-aws
Let child modules implicitly import their parent, instead of the other way around. kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: language definition Relating to the Dafny language definition itself
#5227 opened Mar 21, 2024 by keyboardDrummer
2
Use proof dependencies for more thorough brittleness reduction warnings kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#5261 opened Mar 27, 2024 by atomb
@keyboardDrummer
6
Suggest changes that could reduce brittleness kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#5259 opened Mar 27, 2024 by atomb
@atomb
1
Array initialization as powerful as constructors kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#5258 opened Mar 27, 2024 by MikaelMayer
1
Free statements with ownership tracking kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#5257 opened Mar 27, 2024 by MikaelMayer
Give --resource-limit a default value kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#5254 opened Mar 27, 2024 by keyboardDrummer
3
Warn about potential brittleness due to use of difficult constructs kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#5253 opened Mar 26, 2024 by atomb
@atomb
5
Dafny Encounters internal translation error for nested quantifier expressions when a subtitute is required during 2: compilation of correct program Dafny rejects a valid program during compilation kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: verifier Translation from Dafny to Boogie (translator) priority: next Will consider working on this after in progress work is done
#5250 opened Mar 26, 2024 by arminvakil
predicate subtypes of functions not propagating predicates has-workaround: yes There is a known workaround incompleteness Things that Dafny should be able to prove, but can't
#5245 opened Mar 23, 2024 by erniecohen
3
Incorrectly inferring type as nullable during 2: compilation of correct program Dafny rejects a valid program during compilation kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label priority: now Will work on this now
#5244 opened Mar 22, 2024 by txiang61
@ssomayyajula
1
Enable module resolution caching to work, even if the file containing the module has changed kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: language server Support for LSP in Dafny (server part; client is in ide-vscode repo)
#5241 opened Mar 22, 2024 by keyboardDrummer
@keyboardDrummer
1
Crash on reads with different datatype ordering crash Dafny crashes on this input, or generates malformed code that can not be executed during 1: program development Bad error message or documentation; IDE bug; crash compiling invalid program kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: resolver Resolution and typechecking priority: next Will consider working on this after in progress work is done
#5232 opened Mar 21, 2024 by txiang61
1
@stefan-aws
1
ProTip! Exclude everything labeled bug with -label:bug.