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,030 Open 1,599 Closed
1,030 Open 1,599 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

Missing downcasts invalid translated code The compiler generates invalid code, making the the target language infrastructure crash kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#5597 by RustanLeino was closed Jul 10, 2024 updated Jul 10, 2024
1
@RustanLeino
Nested LetExpr chain compiles to tons of nested Java lambdas, which javac chokes on kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: java Dafny's Java transpiler and its runtime
#3868 by robin-aws was closed Jul 10, 2024 updated Jul 10, 2024
2
3
Bad related error location for inlined conjunct area: error-reporting Clarity of the error reporting kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#5586 by RustanLeino was closed Jul 10, 2024 updated Jul 10, 2024
1
@RustanLeino
Test generation produces sequence with elements of wrong type kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: test generation Relates to the dafny generate-tests command
#5608 by stefan-aws was closed Jul 9, 2024 updated Jul 9, 2024
1
Support for bounded polymorphism / trait bounds kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#5211 by dschoepe was closed Jul 9, 2024 updated Jul 9, 2024
1
internal error on assert/assume (... decreases to ...) crash Dafny crashes on this input, or generates malformed code that can not be executed kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: resolver Resolution and typechecking
#5585 by erniecohen was closed Jul 8, 2024 updated Jul 8, 2024
1
@atomb
Disjunctive pattern matching not correctly handled during 4: bad execution of correct program A bug in the Dafny compiler that causes a correct Dafny program to execute incorrectly kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#5572 by MikaelMayer was closed Jun 26, 2024 updated Jun 26, 2024
1
Flaky test: ConcurrentCompilationDoesNotBreakCaching 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
#5515 by MikaelMayer was closed Jun 26, 2024 updated Jun 26, 2024
1
3
Helpers.unsignedLongToBigInteger removed from Java runtime release-blocker Must be resolved before the next release
#5553 by robin-aws was closed Jun 17, 2024 updated Jun 17, 2024
1
@robin-aws
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 part: resolver Resolution and typechecking priority: next Will consider working on this after in progress work is done
#5365 by erniecohen was closed Jun 14, 2024 updated Jun 14, 2024
1
@MikaelMayer
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 by erniecohen was closed Jun 14, 2024 updated Jun 14, 2024
1
@MikaelMayer
1
[PRERELEASE REGRESSION] Dafny prerelease regression from aws/aws-cryptographic-material-providers-library breaking-change Any change that will cause existing Dafny codebases to break (excluding verification instability)
#5473 by aws-crypto-tools-ci-bot was closed Jun 11, 2024 updated Jun 11, 2024
18
[PRERELEASE REGRESSION] Dafny prerelease regression from smithy-lang/smithy-dafny breaking-change Any change that will cause existing Dafny codebases to break (excluding verification instability)
#5485 by dafny-lang-bot was closed Jun 11, 2024 updated Jun 11, 2024
14
Flaky test: DafnyTestGeneration kind: language development speed Slows down development of Dafny the language, flaky tests
#5549 by MikaelMayer was closed Jun 11, 2024 updated Jun 11, 2024
3
Flaky test Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization.ProjectManagerDatabaseTest.ChangeAndUndoProjectWithMultipleFile kind: language development speed Slows down development of Dafny the language, flaky tests
#5550 by MikaelMayer was closed Jun 10, 2024 updated Jun 10, 2024
1
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 by keyboardDrummer was closed Jun 10, 2024 updated Jun 10, 2024
1
@keyboardDrummer
1
Crash, likely related to refinement area: refinement Dafny's module-refinement machinery 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
#4129 by davidcok was closed Jun 10, 2024 updated Jun 10, 2024
@keyboardDrummer
3
textDocument/codeAction failed during 1: program development Bad error message or documentation; IDE bug; crash compiling invalid program part: language server Support for LSP in Dafny (server part; client is in ide-vscode repo)
#5541 by keyboardDrummer was closed Jun 7, 2024 updated Jun 7, 2024
1
@keyboardDrummer
Nighty failed because a MacOS node timed out 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
#5432 by keyboardDrummer was closed Jun 6, 2024 updated Jun 6, 2024
2
Flaky CI cancelled before completing
#5530 by MikaelMayer was closed Jun 5, 2024 updated Jun 5, 2024
1
Error when guarding nonexistent this 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 lang: c# Dafny's C# transpiler and its runtime release-blocker Must be resolved before the next release
#5523 by fabiomadge was closed Jun 4, 2024 updated Jun 4, 2024
1
Add predicate for definite assignment kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#5251 by atomb was closed Jun 4, 2024 updated Jun 4, 2024
@alex-chew
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 by keyboardDrummer was closed May 30, 2024 updated May 30, 2024
1
@keyboardDrummer
Allow termination ordering to be written in expressions kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#5252 by atomb was closed May 29, 2024 updated May 29, 2024
1
@atomb
"this" not protected in lambdas in tail-recursive functions during 4: bad execution of correct program A bug in the Dafny compiler that causes a correct Dafny program to execute incorrectly kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag priority: next Will consider working on this after in progress work is done
#4684 by RustanLeino was closed May 24, 2024 updated May 24, 2024
1
@fabiomadge
ProTip! Mix and match filters to narrow down what you’re looking for.