-
Notifications
You must be signed in to change notification settings - Fork 257
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
Upcoming changes to Boogie
part: documentation
Dafny's reference manual, tutorial, and other materials
#4005
opened May 14, 2023 by
shazqadeer
Idea: replace attributes with arbitrary expressions
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#3149
opened Dec 2, 2022 by
robin-aws
Allow forall statements in expressions
difficulty: easy
Issues that should take a few days at most to fix
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
part: parser
First phase of Dafny's pipeline
part: verifier
Translation from Dafny to Boogie (translator)
status: designed
Issues that have a complete story on how to implement this feature and why we want it
#146
opened Oct 10, 2017 by
wilcoxjay
Feature request: better termination metrics for functions that recurse on maps
difficulty: medium
Issues that should take a few days to a week to fix
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)
status: needs-decision
The cause of this issue is clear; the team needs to decide whether we want to work on it
#226
opened Jan 10, 2019 by
wilcoxjay
dafny fails to deduce body of function across an abstract module boundary
area: refinement
Dafny's module-refinement machinery
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)
status: needs-decision
The cause of this issue is clear; the team needs to decide whether we want to work on it
#255
opened Jun 7, 2019 by
tjhance
issue in datatype/module name conflict
area: ffi
The {:extern} attribute and otherwise interfacing with code in other languages
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
part: code-generation
Support for transpiling Dafny to another language. If relevant, add a `lang:` tag
#259
opened Jun 10, 2019 by
gancherj
Use :extern to call static variables in a class in C#
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
lang: c#
Dafny's C# transpiler and its runtime
#265
opened Jun 14, 2019 by
phoenix1712
/compile:3 C# compiler doesn't find library DLL and crashes
area: ffi
The {:extern} attribute and otherwise interfacing with code in other languages
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: code-generation
Support for transpiling Dafny to another language. If relevant, add a `lang:` tag
#266
opened Jun 14, 2019 by
mschlaipfer
Dafny fails to verify identical universal statements
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#287
opened Jul 1, 2019 by
tjhance
Constructor should be able to call another constructor
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#295
opened Jul 5, 2019 by
samuelgruetter
Feature request: Ability to state and prove running time
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#298
opened Jul 8, 2019 by
saglam
Dafny can't model C# classes without public constructors
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
#313
opened Jul 11, 2019 by
samuelgruetter
Forgetting a reads clause allows to prove false (not a soundness bug, but room for improvement)
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
part: verifier
Translation from Dafny to Boogie (translator)
#316
opened Jul 12, 2019 by
samuelgruetter
Map Comprehension Heuristics
difficulty: medium
Issues that should take a few days to a week to fix
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
part: resolver
Resolution and typechecking
status: designed
Issues that have a complete story on how to implement this feature and why we want it
#13
opened Jul 22, 2016 by
aferr
Is it safe to use 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
reads this
to say "depends on unspecified external state"?
area: ffi
#322
opened Jul 17, 2019 by
samuelgruetter
trying to alias a module through a module facade doesn't work
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#329
opened Jul 25, 2019 by
tjhance
Support for Rust tests
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#5666
opened Aug 5, 2024 by
MikaelMayer
Predicates containing higher-order assertions behave oddly
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
part: verifier
Translation from Dafny to Boogie (translator)
#359
opened Aug 21, 2019 by
csgordon
noisy error messages can hide the "root cause" precondition error
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
part: verifier
Translation from Dafny to Boogie (translator)
#370
opened Aug 27, 2019 by
tjhance
cannot prove simple facts about functions with opaque read clauses
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
part: verifier
Translation from Dafny to Boogie (translator)
#377
opened Sep 10, 2019 by
tjhance
Dafny should issue a warning when an annotation is not supported
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#395
opened Oct 18, 2019 by
mschlaipfer
Add built-in Map Keys to Seq function
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
#424
opened Nov 12, 2019 by
lavaleri
Don't generate code that can access Dafny runtime internals
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
#440
opened Nov 25, 2019 by
robin-aws
Function values requires exact domain type
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
part: verifier
Translation from Dafny to Boogie (translator)
#445
opened Nov 28, 2019 by
RustanLeino
println statement
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#319
opened Jul 15, 2019 by
ghost
Previous Next
ProTip!
What’s not been updated in a month: updated:<2024-07-06.