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

982 Open 1,521 Closed
982 Open 1,521 Closed
Author
Filter by author
Label
Filter by label
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Milestones
Filter by milestone
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

Add dedicated content on determinism and methods vs. functions to the reference manual part: documentation Dafny's reference manual, tutorial, and other materials priority: next Will consider working on this after in progress work is done
#5372 opened Apr 26, 2024 by robin-aws
internal error on static constants in newtypes based on bitvectors kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#5371 opened Apr 26, 2024 by erniecohen
Surprising Verification Failures with Nested Datatypes + Classes kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#5370 opened Apr 26, 2024 by whonore
Crash in new resolver 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: next Will consider working on this after in progress work is done
#5369 opened Apr 26, 2024 by keyboardDrummer
internal error on trait functions taking multiple arguments of trait type parameter 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: next Will consider working on this after in progress work is done
#5368 opened Apr 26, 2024 by erniecohen
2
function refinement broken 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: next Will consider working on this after in progress work is done
#5366 opened Apr 25, 2024 by erniecohen
1
internal error: function call on datatype with updated member 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: next Will consider working on this after in progress work is done
#5365 opened Apr 25, 2024 by erniecohen
Clarify handling of strings in print statement part: documentation Dafny's reference manual, tutorial, and other materials
#5364 opened Apr 25, 2024 by robin-aws
@robin-aws
Behavior of havoc operator in combination with definite assignment is not well explained in error messages during 1: program development Bad error message or documentation; IDE bug; crash compiling invalid program kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#5362 opened Apr 25, 2024 by keyboardDrummer
Request textDocument/completion failed in IDE 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: 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
#5357 opened Apr 24, 2024 by keyboardDrummer
@keyboardDrummer
Spurious Cyclic Datatype Dependency Warning 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: next Will consider working on this after in progress work is done
#5356 opened Apr 24, 2024 by whonore
IDE throws exception related to code actions 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: language server Support for LSP in Dafny (server part; client is in ide-vscode repo)
#5355 opened Apr 24, 2024 by keyboardDrummer
Ensure Dafny runtime libraries are backwards compatible within major versions
#5352 opened Apr 23, 2024 by robin-aws
Allow verifying against a library version X, but running against a newer version X+N kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#5349 opened Apr 23, 2024 by keyboardDrummer Library support
map display vs map update 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
#5351 opened Apr 23, 2024 by kjx
3
Standard libraries not working with general-newtypes=true 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
#5345 opened Apr 22, 2024 by MikaelMayer
1
1
Enable reusing the specification of options in a dfyconfig.toml 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
#5337 opened Apr 19, 2024 by keyboardDrummer
1
2
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
3
Internal Error: System.NullReferenceException crash Dafny crashes on this input, or generates malformed code that can not be executed 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: resolver Resolution and typechecking priority: next Will consider working on this after in progress work is done
#5331 opened Apr 17, 2024 by erniecohen
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
#5330 opened Apr 17, 2024 by MikaelMayer
1
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
#5321 opened Apr 15, 2024 by keyboardDrummer
Unstable test 'VerificationDiagnosticsCanBeMigratedAcrossMultipleResolutions kind: language development speed Slows down development of Dafny the language
#5319 opened Apr 12, 2024 by keyboardDrummer
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
ProTip! Updated in the last three days: updated:>2024-04-23.