-
Notifications
You must be signed in to change notification settings - Fork 258
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
More flexible new type definition
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
priority: not yet
Will reconsider working on this when we're looking for work
#479
opened Jan 8, 2020 by
davidcok
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
priority: not yet
Will reconsider working on this when we're looking for work
#395
opened Oct 18, 2019 by
mschlaipfer
"compilation of seq<TRAIT> is not supported"; consider introducing a ghost
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
priority: not yet
Will reconsider working on this when we're looking for work
#406
opened Oct 28, 2019 by
robin-aws
Opaque functions cause failing override checks
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
part: verifier
Translation from Dafny to Boogie (translator)
priority: not yet
Will reconsider working on this when we're looking for work
#422
opened Nov 12, 2019 by
RustanLeino
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
priority: not yet
Will reconsider working on this when we're looking for work
#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
priority: not yet
Will reconsider working on this when we're looking for work
#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)
priority: not yet
Will reconsider working on this when we're looking for work
#445
opened Nov 28, 2019 by
RustanLeino
Support calling Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
part: language definition
Relating to the Dafny language definition itself
priority: not yet
Will reconsider working on this when we're looking for work
ToString
on an arbitrary value
kind: enhancement
#450
opened Dec 3, 2019 by
robin-aws
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
priority: not yet
Will reconsider working on this when we're looking for work
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
Compiled Dafny methods can be invoked in target language without satisfying preconditions
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
priority: not yet
Will reconsider working on this when we're looking for work
#461
opened Dec 16, 2019 by
robin-aws
Post-conditions assumed true for externally-implemented methods
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
priority: not yet
Will reconsider working on this when we're looking for work
#463
opened Dec 16, 2019 by
robin-aws
Inferred types not qualified in parseable program output
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
part: printer
Pretty printer for Dafny's AST
priority: not yet
Will reconsider working on this when we're looking for work
#465
opened Dec 18, 2019 by
robin-aws
New annotation to give an externally-visible name to a generated Dafny class
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
priority: not yet
Will reconsider working on this when we're looking for work
#469
opened Dec 30, 2019 by
lukemaurer
/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
priority: not yet
Will reconsider working on this when we're looking for work
#266
opened Jun 14, 2019 by
mschlaipfer
Integer multiplication errors
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
part: verifier
Translation from Dafny to Boogie (translator)
priority: not yet
Will reconsider working on this when we're looking for work
#488
opened Jan 10, 2020 by
echuber2
Dafny Java runtime should be published as a Maven artifact
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
lang: java
Dafny's Java transpiler and its runtime
part: runtime
Happens in Dafny's runtime (Add a `lang` tag if relevant)
priority: not yet
Will reconsider working on this when we're looking for work
#492
opened Jan 10, 2020 by
robin-aws
Dafny Javascript runtime (Binaries/DafnyRuntime.js) should be published as an npm package
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
lang: js
Dafny's JavaScript transpiler and its runtime
part: runtime
Happens in Dafny's runtime (Add a `lang` tag if relevant)
priority: not yet
Will reconsider working on this when we're looking for work
#493
opened Jan 10, 2020 by
robin-aws
Dafny Go runtime (Binaries/DafnyRuntime.go) should be published as a Go module
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
lang: golang
Dafny's transpiler to Go and its runtime
part: runtime
Happens in Dafny's runtime (Add a `lang` tag if relevant)
priority: not yet
Will reconsider working on this when we're looking for work
#494
opened Jan 10, 2020 by
robin-aws
Outstanding issues with Dafny test support
part: documentation
Dafny's reference manual, tutorial, and other materials
priority: not yet
Will reconsider working on this when we're looking for work
#451
opened Dec 4, 2019 by
robin-aws
Use variable order in {:inductive} attribute.
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: verifier
Translation from Dafny to Boogie (translator)
priority: not yet
Will reconsider working on this when we're looking for work
status: designed
Issues that have a complete story on how to implement this feature and why we want it
#34
opened Sep 27, 2016 by
richardlford
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)
priority: not yet
Will reconsider working on this when we're looking for work
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)
priority: not yet
Will reconsider working on this when we're looking for work
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)
priority: not yet
Will reconsider working on this when we're looking for work
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
priority: not yet
Will reconsider working on this when we're looking for work
#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
priority: not yet
Will reconsider working on this when we're looking for work
#265
opened Jun 14, 2019 by
phoenix1712
ProTip!
Adding no:label will show everything without a label.