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
29 Open 29 Closed
29 Open 29 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

Using --default-function-opacity=AutoRevealDependencies can perform badly 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: verifier Translation from Dafny to Boogie (translator) priority: not yet Will reconsider working on this when we're looking for work
#5272 opened Mar 28, 2024 by atomb
Use proof dependencies for more thorough brittleness reduction warnings kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#5261 opened Mar 27, 2024 by atomb
@keyboardDrummer
6
Suggest changes that could reduce brittleness kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#5259 opened Mar 27, 2024 by atomb
@atomb
1
Warn about potential brittleness due to use of difficult constructs kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#5253 opened Mar 26, 2024 by atomb
@atomb
5
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
1
@atomb
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
@alex-chew
Make it possible to write at least some of Dafny's prelude axioms in Dafny kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#5198 opened Mar 14, 2024 by atomb
@atomb
1
Automate extracting an expression into a separately-defined function kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#5197 opened Mar 14, 2024 by atomb
1
Module refinement leads to resolution errors with --default-function-opacity AutoRevealDependencies 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: not yet Will reconsider working on this when we're looking for work
#5196 opened Mar 14, 2024 by atomb
Add by blocks to function and method calls area: performance Performance issues 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: language definition Relating to the Dafny language definition itself
#5192 opened Mar 13, 2024 by atomb
19
Add --solver-option-help flag kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#5186 opened Mar 12, 2024 by atomb
1
Add --attribute-help flag kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#5185 opened Mar 12, 2024 by atomb
1
Document HTML verification coverage reports part: documentation Dafny's reference manual, tutorial, and other materials
#5182 opened Mar 12, 2024 by atomb
@atomb
Dafny hangs when verifying certain code kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label release-blocker Must be resolved before the next release
#5154 by atomb was closed Mar 12, 2024
2
Add incremental verification progress reporting in a Dafny-centric way kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#5150 by atomb was closed Mar 22, 2024
1
2
Type mismatch allowed in ensures clause with type parameters and datatypes 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
#5144 opened Mar 4, 2024 by atomb
5
Hang with dafny verify on Std 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
#5088 by atomb was closed Apr 24, 2024
6
Spurious warnings about contradictory assumptions in types kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#5029 by atomb was closed Jan 31, 2024
1
Remove multiplication of resource count by 1000 area: new users Getting new users started difficulty: easy Issues that should take a few days at most to fix has-workaround: yes There is a known workaround kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label misc: cleanup Cleanups in the implementation or in corners of the language part: verifier Translation from Dafny to Boogie (translator) status: needs-decision The cause of this issue is clear; the team needs to decide whether we want to work on it
#4962 by atomb was closed Jan 19, 2024
1
@atomb
2
Support verification logs in JSON format kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#4907 by atomb was closed Jan 11, 2024
1
@atomb
5
Crash when running -testContracts on refinement of abstract module 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
#4845 by atomb was closed Jan 4, 2024
1
@atomb
3
The %verify lit command fails to find Z3 during deep tests area: build-system Support for dependencies in Dafny, generation of target language build files kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: ci Issue is with Dafny's CI infrastructure
#4608 by atomb was closed Oct 22, 2023
1
1
Error when collection cardinality used as a long in Java difficulty: easy Issues that should take a few days at most to fix 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 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
#4483 by atomb was closed Aug 30, 2023
1
@atomb
Misleading error with method call for field assignment in constructor area: error-reporting Clarity of the error reporting during 1: program development Bad error message or documentation; IDE bug; crash compiling invalid program has-workaround: yes There is a known workaround kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: resolver Resolution and typechecking priority: not yet Will reconsider working on this when we're looking for work
#4383 opened Aug 3, 2023 by atomb
Can't use SOLVER=noop with Dafny kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#4196 by atomb was closed Apr 12, 2024
@atomb
2
ProTip! Exclude everything labeled bug with -label:bug.