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,021 Open 1,591 Closed
1,021 Open 1,591 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

Enable hiding of functions to an extend that it could make opaque obsolete
#5575 opened Jun 25, 2024 by keyboardDrummer
@keyboardDrummer
1
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 opened Jun 25, 2024 by MikaelMayer
1
Malformed Boogie for if-then-else with non-reference traits kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#5570 opened Jun 24, 2024 by RustanLeino
Ordering problem in Python code generator kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: python Dafny's Python transpiler and its runtime part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag
#5569 opened Jun 24, 2024 by RustanLeino
Integrate MIRI as part of the CI to ensure no memory leak in the DafnyRuntimeRust
#5567 opened Jun 21, 2024 by MikaelMayer
[PRERELEASE REGRESSION] Dafny prerelease regression from aws/aws-cryptographic-material-providers-library
#5565 opened Jun 18, 2024 by aws-crypto-tools-ci-bot
7
Dafny-to-Rust code generator part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag priority: now Will work on this now
#5561 opened Jun 14, 2024 by MikaelMayer
7 tasks
Make the Rust compiler run on nightly once it passes all tests part: ci Issue is with Dafny's CI infrastructure part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag priority: now Will work on this now
#5560 opened Jun 14, 2024 by MikaelMayer
C# and Go Backends: Incorrect finite map semantics 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 lang: golang Dafny's transpiler to Go and its runtime lang: js Dafny's JavaScript transpiler and its runtime priority: not yet Will reconsider working on this when we're looking for work
#5557 opened Jun 12, 2024 by khemichew
1
Potential enhancement: array initialisation that is incompatible with declared size 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 kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny priority: not yet Will reconsider working on this when we're looking for work
#5556 opened Jun 12, 2024 by khemichew
Dafny generated code not necessarily backwards compatible with code generated by older Dafny versions kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label priority: now Will work on this now release-blocker Must be resolved before the next release
#5555 opened Jun 12, 2024 by robin-aws
@robin-aws
4
C# backend: Multiset size overflow 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 lang: c# Dafny's C# transpiler and its runtime priority: not yet Will reconsider working on this when we're looking for work
#5554 opened Jun 12, 2024 by khemichew
JavaScript and Go backend: Incorrect map cardinality kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: golang Dafny's transpiler to Go and its runtime lang: js Dafny's JavaScript transpiler and its runtime part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag priority: not yet Will reconsider working on this when we're looking for work
#5552 opened Jun 12, 2024 by khemichew
1
Flaky test: Unspecified kind: language development speed Slows down development of Dafny the language, flaky tests part: ci Issue is with Dafny's CI infrastructure priority: not yet Will reconsider working on this when we're looking for work
#5551 opened Jun 11, 2024 by MikaelMayer
Named ensure clause 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 priority: not yet Will reconsider working on this when we're looking for work
#5544 opened Jun 7, 2024 by keyboardDrummer
can't label assumptions 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 priority: not yet Will reconsider working on this when we're looking for work
#5540 opened Jun 7, 2024 by kjx
can't label forall-ensuring statement 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 priority: not yet Will reconsider working on this when we're looking for work
#5539 opened Jun 7, 2024 by kjx
Unstable CLI test git-issues/git-issue-697j.dfy, related to Rust backend kind: language development speed Slows down development of Dafny the language, flaky tests part: ci Issue is with Dafny's CI infrastructure priority: not yet Will reconsider working on this when we're looking for work
#5537 opened Jun 6, 2024 by keyboardDrummer
5
Costless by clause in assert .. by { } when using --isolate-assertions 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 priority: not yet Will reconsider working on this when we're looking for work
#5536 opened Jun 6, 2024 by keyboardDrummer
@keyboardDrummer
3
Verification hang apparently caused by Std import 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: not yet Will reconsider working on this when we're looking for work
#5534 opened Jun 6, 2024 by nverhaaren
3
Issue with multi-backend-testing kind: language development speed Slows down development of Dafny the language, flaky tests priority: not yet Will reconsider working on this when we're looking for work
#5533 opened Jun 5, 2024 by MikaelMayer
Bad encoding for this in tail recursive functions when compiling to Java 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: java Dafny's Java transpiler and its runtime priority: not yet Will reconsider working on this when we're looking for work
#5532 opened Jun 5, 2024 by fabiomadge
1
assertion of map values fails when same postcondition succeeds (or if preceded by Keys assertion) incompleteness Things that Dafny should be able to prove, but can't kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: verifier Translation from Dafny to Boogie (translator) priority: not yet Will reconsider working on this when we're looking for work
#5527 opened Jun 5, 2024 by kjx
2
Verification ignores resource limits kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: z3 Issue is in Z3 priority: not yet Will reconsider working on this when we're looking for work
#5525 opened Jun 4, 2024 by hmijail
6
Constraint-less newtypes assumed to be nonempty 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
#5521 opened Jun 3, 2024 by RustanLeino
1
@RustanLeino
ProTip! Type g p on any issue or pull request to go back to the pull request listing page.