-
Notifications
You must be signed in to change notification settings - Fork 256
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
Report errors originating from included files when verifying including file
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#16
by plaidfinch
was closed Jan 14, 2017
feature request: improved char type
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#4
by Chris-Hawblitzel
was closed Jan 10, 2017
feature request: naming function return values
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#5
by Chris-Hawblitzel
was closed Jan 20, 2017
feature request: declaring constants
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#6
by Chris-Hawblitzel
was closed Nov 30, 2016
feature request: for loops
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#7
by calder
was closed Jul 8, 2020
missing "ghost" keywords when printing expressions in methods
#8
by danmatichuk
was closed Jul 12, 2016
/trace output is less helpful than it could be due to buffering
#10
by 0xabu
was closed Jul 15, 2016
Compilation Error: generates duplicate local variable declarations
#15
by laurejt
was closed Jul 26, 2016
Cross-module export causes compile error
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#17
by danmatichuk
was closed Jan 12, 2017
crash in Microsoft.Dafny.Resolver.FreeVariables
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#18
by 0xabu
was closed Oct 5, 2016
quantifiers over types that might be heap types
difficulty: hard
Issues that will take more than a week to fix
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
logic
An inconsistency in Dafny's logic (e.g. in the Boogie prelude)
part: verifier
Translation from Dafny to Boogie (translator)
#19
by Chris-Hawblitzel
was closed Feb 23, 2023
Dafny fails, but returns exit status of zero
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#21
by 0xabu
was closed Sep 22, 2016
Translation error when using sets in a forall expression; bad triggers?
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#22
by 0xabu
was closed Oct 5, 2016
Crash (assertion failure) in Dafny.Translator.FuelSetting.GetFunctionFuel
#23
by 0xabu
was closed Sep 1, 2016
function lemma in "ensures" doesn't work in 1.9.8 (worked in 1.9.7)
has-workaround: yes
There is a known workaround
incompleteness
Things that Dafny should be able to prove, but can't
part: verifier
Translation from Dafny to Boogie (translator)
#25
by xinhaoyuan
was closed May 11, 2022
Test generation produces sequence with elements of wrong type
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
part: test generation
Relates to the dafny generate-tests command
#5608
by stefan-aws
was closed Jul 9, 2024
Previous Next
ProTip!
Follow long discussions with comments:>50.