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
52 Open 42 Closed
52 Open 42 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

JSON log inaccuracies area: error-reporting Clarity of the error reporting 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
#5718 opened Aug 23, 2024 by hmijail
4
Better path error reporting area: error-reporting Clarity of the error reporting kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: verifier Translation from Dafny to Boogie (translator)
#5628 opened Jul 16, 2024 by keyboardDrummer
Malformed DafnyPrelude causes silent failure and reports success area: error-reporting Clarity of the error reporting 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
#5592 opened Jul 1, 2024 by RustanLeino
non-non-non-optional semicolons give horrible error messages - LOW SEVERITY area: error-reporting Clarity of the error reporting 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
#5403 opened May 6, 2024 by kjx
3
Add X-is-a-statement-not-an-expression error messages area: error-reporting Clarity of the error reporting kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#5047 opened Feb 2, 2024 by RustanLeino
Parse error when matching over constant from imported module area: error-reporting Clarity of the error reporting kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: parser First phase of Dafny's pipeline
#5009 opened Jan 24, 2024 by jtristan
3
Unintuitive error location for errors on explicitly included dependency files area: error-reporting Clarity of the error reporting
#4977 opened Jan 11, 2024 by Rekkonnect
10
Failed to infer subtype implicitly area: error-reporting Clarity of the error reporting difficulty: easy Issues that should take a few days at most to fix 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: resolver Resolution and typechecking priority: next Will consider working on this after in progress work is done status: fixed Issue cannot be reproduced with latest Dafny release
#4968 opened Jan 9, 2024 by txiang61
3
Failure to Prove Existential with Subsequence area: error-reporting Clarity of the error reporting 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
#4920 opened Dec 29, 2023 by whonore
8
Cannot use a smaller reads clause in a class that extends a trait area: error-reporting Clarity of the error reporting kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#4822 opened Nov 28, 2023 by jorge-jbs
3
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
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
Invalid unicode give unhelpful error message area: error-reporting Clarity of the error reporting kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: parser First phase of Dafny's pipeline
#4117 opened Jun 2, 2023 by davidcok
Inconsistent command-line error messages area: error-reporting Clarity of the error reporting kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#4072 opened May 24, 2023 by davidcok
Comma-separated expressions using <, > operators parsed as type area: error-reporting Clarity of the error reporting part: parser First phase of Dafny's pipeline
#3932 opened May 1, 2023 by alex-usher
6
forall-ensures not quite equivalent to assert-by area: error-reporting Clarity of the error reporting 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
#3559 opened Feb 17, 2023 by davidcok
@davidcok
2
Wrong cyclic dependency error reported area: error-reporting Clarity of the error reporting kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: resolver Resolution and typechecking
#3271 opened Dec 25, 2022 by MikaelMayer
1
Can't prove modifies clause area: error-reporting Clarity of the error reporting incompleteness Things that Dafny should be able to prove, but can't
#3265 opened Dec 23, 2022 by MikaelMayer
1
@MikaelMayer
2
[Bug]: Unknown /compileTarget is silently ignored; should be an error area: error-reporting Clarity of the error reporting part: CLI interacting with Dafny on the command line
#2988 opened Nov 4, 2022 by mattmccutchen-amazon
Function precondition might not hold without hint area: error-reporting Clarity of the error reporting 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)
#2918 opened Oct 24, 2022 by MikaelMayer
Can we warn about curly braces in mistyped expression-level ifs? area: error-reporting Clarity of the error reporting kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: resolver Resolution and typechecking
#2899 opened Oct 17, 2022 by cpitclaudel
12
/warnMissingConstructorParentheses not warning on example area: error-reporting Clarity of the error reporting kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: resolver Resolution and typechecking
#2897 opened Oct 14, 2022 by mschlaipfer
@keyboardDrummer
1
Imprecision in warnMissingConstructorParentheses? area: error-reporting Clarity of the error reporting kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: resolver Resolution and typechecking
#2896 opened Oct 14, 2022 by cpitclaudel
@keyboardDrummer
Incompatible plugin could have better error reporting area: error-reporting Clarity of the error reporting kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#2886 opened Oct 12, 2022 by MikaelMayer
Add a boogie command line as a comment when emitting a .bpl file area: error-reporting Clarity of the error reporting 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
#2800 opened Sep 26, 2022 by davidcok
ProTip! Type g i on any issue or pull request to go back to the issue listing page.