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
49 Open 82 Closed
49 Open 82 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

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
Unstable test: "DafnyTestGeneration.Test" test run gets cancelled, possibly due to taking too long 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
#5488 opened May 24, 2024 by keyboardDrummer
@robin-aws
9
Missing autocut step from some downstream customer nightly tests priority: next Will consider working on this after in progress work is done release-blocker Must be resolved before the next release
#5379 opened Apr 29, 2024 by robin-aws
@robin-aws
function refinement broken area: refinement Dafny's module-refinement machinery 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 part: resolver Resolution and typechecking priority: next Will consider working on this after in progress work is done
#5366 opened Apr 25, 2024 by erniecohen
@robin-aws
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
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
Python fails to cast Main arguments as strings correctly in --unicode-char:true mode 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: python Dafny's Python transpiler and its runtime 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
#5184 opened Mar 12, 2024 by robin-aws
@robin-aws
Crash on running a program on the library backend 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 priority: not yet Will reconsider working on this when we're looking for work
#5156 opened Mar 7, 2024 by robin-aws
@robin-aws
2
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
1
@robin-aws
1
Support --unicode-char:false with --standard-libraries has-workaround: no There are no known workarounds
#5003 opened Jan 23, 2024 by robin-aws
@robin-aws
1
Add --include-standard-libraries option to dafny translate kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: CLI interacting with Dafny on the command line
#5002 opened Jan 23, 2024 by robin-aws
@robin-aws
1
Handle --coverage-report with dafny translate (or legacy compilation option) kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#4965 opened Jan 9, 2024 by codyroux
@robin-aws
6
Include directives can lead to including unverified code in 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 part: tools Tools built on top of Dafny
#4762 opened Nov 9, 2023 by robin-aws
2
@robin-aws
1
Standard library: Interop kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: standard libraries Standard libraries packaged in the Dafny distribution
#4654 opened Oct 11, 2023 by robin-aws
@robin-aws
Standard library: Actions kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: standard libraries Standard libraries packaged in the Dafny distribution
#4646 opened Oct 11, 2023 by robin-aws
@robin-aws
1
Feature request: support {:termination false} on classes as well as traits kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: resolver Resolution and typechecking
#4642 opened Oct 11, 2023 by robin-aws
@robin-aws
Allow more assumptions when building .doo files kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#4517 opened Sep 5, 2023 by robin-aws
@robin-aws
Name conflict in creating a .doo archive 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
#4068 opened May 23, 2023 by davidcok
@robin-aws
Adding a check that libraries verify to nightly testing
#4034 opened May 17, 2023 by davidcok Loading…
@robin-aws
3
Re-add including-doo.dfy test file kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#3984 opened May 10, 2023 by robin-aws
@robin-aws
1
Detect and report use of mixing options that change semantics crash Dafny crashes on this input, or generates malformed code that can not be executed 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: pre-2012 invalid translated code The compiler generates invalid code, making the the target language infrastructure crash kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny logic An inconsistency in Dafny's logic (e.g. in the Boogie prelude) priority: not yet Will reconsider working on this when we're looking for work
#3556 opened Feb 16, 2023 by davidcok Library support
@robin-aws
4
Support easy configuration of alternate Z3 version when installing Dafny kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#3478 opened Feb 7, 2023 by robin-aws
@robin-aws
2
Output encoding for Java kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: java Dafny's Java transpiler and its runtime part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag
#3344 opened Jan 9, 2023 by fabiomadge
@robin-aws
Consistency in array-length limits kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag
#3212 opened Dec 16, 2022 by RustanLeino
@robin-aws
3
Enable Dafny support in Gradle 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
#3169 opened Dec 9, 2022 by keyboardDrummer Library support
@robin-aws
2
ProTip! Add no:assignee to see everything that’s not assigned.