-
Notifications
You must be signed in to change notification settings - Fork 254
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.
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
Author
Label
Projects
Milestones
Assignee
Sort
Issues list
Ghost code incorrectly rendered
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#3278
opened Dec 27, 2022 by
MikaelMayer
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
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
Error ranges include non-relevant places
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)
#3176
opened Dec 11, 2022 by
MikaelMayer
Error highlighted at the default parameter site instead of the call site
part: language server
Support for LSP in Dafny (server part; client is in ide-vscode repo)
#3170
opened Dec 9, 2022 by
MikaelMayer
[Feature request]: Assert simplification calculus (a.k.a. verification debugging or "Move assert up") with Code Actions
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#3114
opened Nov 25, 2022 by
MikaelMayer
[Feature request]: Weakest Precondition calculus (a.k.a. verification debugging or "Move assert up") with Code Actions
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)
#3102
opened Nov 23, 2022 by
MikaelMayer
[Feature request]: Name assertions in functions
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#3101
opened Nov 23, 2022 by
MikaelMayer
Misleading "verified" gutter icon
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)
#3076
opened Nov 18, 2022 by
MikaelMayer
Implementations missings
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#3071
opened Nov 17, 2022 by
MikaelMayer
[Bug]: Cannot declare extern ToString in C#
area: ffi
The {:extern} attribute and otherwise interfacing with code in other languages
lang: c#
Dafny's C# transpiler and its runtime
part: code-generation
Support for transpiling Dafny to another language. If relevant, add a `lang:` tag
#3039
opened Nov 10, 2022 by
MikaelMayer
[Feature request]: Documentation on hover
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)
[Feature request]: Generate explicit assertions
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)
Unsound use of A bug in the Dafny compiler that causes a correct Dafny program to execute incorrectly
introduced: pre-2012
{this}
in constant initialization
during 4: bad execution of correct program
#2923
opened Oct 25, 2022 by
MikaelMayer
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
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
Missing where clause on handle types and incorrect subtyping checks on maps containing arrows
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
part: resolver
Resolution and typechecking
part: verifier
Translation from Dafny to Boogie (translator)
#2835
opened Oct 3, 2022 by
MikaelMayer
Crash in translation to Boogie
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
part: verifier
Translation from Dafny to Boogie (translator)
#2584
opened Aug 12, 2022 by
MikaelMayer
Undeclared top-level issue
area: error-reporting
Clarity of the error reporting
#2550
opened Aug 4, 2022 by
MikaelMayer
Bug: Internal parse error.
part: language server
Support for LSP in Dafny (server part; client is in ide-vscode repo)
#2466
opened Jul 21, 2022 by
MikaelMayer
Dafny 4.0 suggestion: Line and Column indexed the same
breaking-change
Any change that will cause existing Dafny codebases to break (excluding verification instability)
#2452
opened Jul 19, 2022 by
MikaelMayer
Unstable priority ordering test
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#2422
opened Jul 15, 2022 by
MikaelMayer
Dafny 4.0 suggestion: Break up {:extern} and support language specificities
area: ffi
The {:extern} attribute and otherwise interfacing with code in other languages
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
misc: language proposals
Proposals for change to the language that go beyon simple enhancement requests
#2397
opened Jul 12, 2022 by
MikaelMayer
Dafny 4 suggestion: Replace subset types "type" by "predicate type"
breaking-change
Any change that will cause existing Dafny codebases to break (excluding verification instability)
misc: language proposals
Proposals for change to the language that go beyon simple enhancement requests
#2368
opened Jul 6, 2022 by
MikaelMayer
Assertion splits should display related locations
area: error-reporting
Clarity of the error reporting
part: verifier
Translation from Dafny to Boogie (translator)
#2348
opened Jul 1, 2022 by
MikaelMayer
ProTip!
Type g i on any issue or pull request to go back to the issue listing page.