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

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 updated Jun 24, 2024
@robin-aws
9
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 updated Jun 24, 2024
@robin-aws
4
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 updated May 14, 2024
@robin-aws
2
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 updated May 6, 2024
2
@robin-aws
1
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 updated Apr 30, 2024
@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 updated Apr 29, 2024
@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 updated Apr 25, 2024
@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 updated Apr 23, 2024
@robin-aws
2
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 updated Apr 23, 2024
@robin-aws
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 updated Apr 23, 2024
@robin-aws
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 updated Apr 16, 2024 Library support
@robin-aws
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 updated Feb 21, 2024 Library support
@robin-aws
4
Assert failing in strange way kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny misc: brittleness When Dafny sometimes proves something, and sometimes doesn't part: verifier Translation from Dafny to Boogie (translator)
#1570 opened Nov 6, 2021 by hmijail updated Feb 7, 2024
@robin-aws
10
rise4fun can't open now,is there any backup link? kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny misc: cleanup Cleanups in the implementation or in corners of the language
#1344 opened Aug 10, 2021 by Aaron-clou updated Feb 7, 2024
@robin-aws
1
DafnyPipeline.Test build error kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label kind: language development speed Slows down development of Dafny the language, flaky tests misc: cleanup Cleanups in the implementation or in corners of the language
#1565 opened Nov 5, 2021 by hirataqdees updated Feb 7, 2024
@robin-aws
3
Provide targeted test cases for new compilers kind: language development speed Slows down development of Dafny the language, flaky tests misc: cleanup Cleanups in the implementation or in corners of the language
#1776 opened Feb 1, 2022 by robin-aws updated Feb 7, 2024
@robin-aws
Move runtimes into distinct project in the solution kind: language development speed Slows down development of Dafny the language, flaky tests
#1530 opened Oct 22, 2021 by camrein updated Feb 7, 2024
@robin-aws
5
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 updated Feb 6, 2024
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 updated Feb 1, 2024
@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 updated Jan 11, 2024
@robin-aws
6
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 updated Nov 13, 2023
@robin-aws
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 updated Nov 8, 2023
@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 updated Nov 8, 2023
@robin-aws
1
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 updated Sep 6, 2023
@robin-aws
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 updated Jul 9, 2023
@robin-aws
2
ProTip! Type g i on any issue or pull request to go back to the issue listing page.