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
87 Open 125 Closed
87 Open 125 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

Cannot prove termination of datatype / seq / generics 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 makes-mikael-grateful This issue, is fixed, would make Mikael Mayer grateful part: verifier Translation from Dafny to Boogie (translator) priority: next Will consider working on this after in progress work is done
#4783 opened Nov 15, 2023 by MikaelMayer
@MikaelMayer
Crash in Boogie when using disable-nonlinear-arithmetic during 2: compilation of correct program Dafny rejects a valid program during compilation has-workaround: yes There is a known workaround kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: boogie Happens after passing the program to Boogie priority: next Will consider working on this after in progress work is done
#4760 opened Nov 9, 2023 by MikaelMayer
6
this is not fresh and fresh in well-formedness 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: v4.1.0 kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label makes-mikael-grateful This issue, is fixed, would make Mikael Mayer grateful part: verifier Translation from Dafny to Boogie (translator) priority: next Will consider working on this after in progress work is done
#4700 opened Oct 20, 2023 by MikaelMayer
1
5
Do not raise an error when reveal mentions an already transparent function, only a warning kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#4562 opened Sep 18, 2023 by MikaelMayer
2
Verification symbols not correct when a declaration is marked {:only} 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
#4544 opened Sep 13, 2023 by MikaelMayer
6
Upgrade reads and modifies error messages area: error-reporting Clarity of the error reporting part: documentation Dafny's reference manual, tutorial, and other materials
#4485 opened Aug 29, 2023 by MikaelMayer
Impossible to specify type characteristics when export provides 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
#4379 opened Aug 3, 2023 by MikaelMayer
Opaque least/greatest predicates not implemented yet kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#4249 opened Jul 5, 2023 by MikaelMayer
1
Impossible to trigger map extensionality kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#4165 opened Jun 11, 2023 by MikaelMayer
Ghost unary function initialized() kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#3974 opened May 8, 2023 by MikaelMayer
3
Cannot prove extremely simple equality already stated. has-workaround: yes There is a known workaround incompleteness Things that Dafny should be able to prove, but can't kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#3863 opened Apr 12, 2023 by MikaelMayer
6
Export/Provides/Reveals not respecting opaqueness kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: verifier Translation from Dafny to Boogie (translator)
#3833 opened Apr 3, 2023 by MikaelMayer
CI fails often on DafnyTestGeneration.Test.Collections.SeqOfObjects kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#3828 opened Mar 30, 2023 by MikaelMayer
@atomb
2
No more intermediate display of assertion when {:vcs_split_on_every_assert} 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)
#3820 opened Mar 29, 2023 by MikaelMayer
Assertions/reveal localized in expressions kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#3806 opened Mar 27, 2023 by MikaelMayer
2
Revealing does not work kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#3805 opened Mar 27, 2023 by MikaelMayer
Hovering information missing 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)
#3774 opened Mar 21, 2023 by MikaelMayer
Cannot extract newtype information 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)
#3536 opened Feb 14, 2023 by MikaelMayer
Optimize BigInteger constant computation kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny lang: c# Dafny's C# transpiler and its runtime 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
#3453 opened Feb 3, 2023 by MikaelMayer
1
Request: Formatter to emit proven fine-grained edits kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: language server Support for LSP in Dafny (server part; client is in ide-vscode repo)
#3415 opened Jan 26, 2023 by MikaelMayer
Feat: Inner methods / closures modifying the heap kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#3392 opened Jan 23, 2023 by MikaelMayer
6
Feature request: Have a way to obtain the skeleton of {:extern} statements kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#3367 opened Jan 13, 2023 by MikaelMayer
TokenWrapper to be a concrete all-in-one-class instead of the token hierarchy kind: language development speed Slows down development of Dafny the language, flaky tests status: designed Issues that have a complete story on how to implement this feature and why we want it
#3354 opened Jan 11, 2023 by MikaelMayer
4
Code action issue to inline postcondition 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)
#3308 opened Jan 3, 2023 by MikaelMayer
@MikaelMayer
Refactoring needed: Replace "Tok" with a format kind: language development speed Slows down development of Dafny the language, flaky tests
#3290 opened Dec 29, 2022 by MikaelMayer
ProTip! Type g i on any issue or pull request to go back to the issue listing page.