-
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
Cannot always prove that a method leaves a disjoint set of objects unmodified
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#608
opened Apr 30, 2020 by
danmatichuk
Provide regular point releases for Dafny from master
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#606
opened Apr 30, 2020 by
robin-aws
Emit Rust code
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#601
opened Apr 20, 2020 by
johnterickson
Feature Request: Support trait types as a type parameter
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#599
opened Apr 17, 2020 by
acioc
Malformed Java target code for unreachable code
crash
Dafny crashes on this input, or generates malformed code that can not be executed
lang: java
Dafny's Java transpiler and its runtime
part: code-generation
Support for transpiling Dafny to another language. If relevant, add a `lang:` tag
#540
opened Feb 12, 2020 by
RustanLeino
C# compiler error when generated lambda refers to out parameter
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
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
#531
opened Feb 5, 2020 by
lukemaurer
Java compiler produces constructors that won't play well with native Java code
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
lang: java
Dafny's Java transpiler and its runtime
#502
opened Jan 14, 2020 by
davidcok
Support releasing Dafny packages as .NET DLLs
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
#501
opened Jan 14, 2020 by
robin-aws
4 of 8 tasks
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)
#494
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)
#493
opened Jan 10, 2020 by
robin-aws
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)
#492
opened Jan 10, 2020 by
robin-aws
Integer multiplication errors
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
part: verifier
Translation from Dafny to Boogie (translator)
#488
opened Jan 10, 2020 by
echuber2
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
#479
opened Jan 8, 2020 by
davidcok
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
#469
opened Dec 30, 2019 by
lukemaurer
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
#465
opened Dec 18, 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
#463
opened Dec 16, 2019 by
robin-aws
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
#461
opened Dec 16, 2019 by
robin-aws
Outstanding issues with Dafny test support
part: documentation
Dafny's reference manual, tutorial, and other materials
#451
opened Dec 4, 2019 by
robin-aws
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
ToString
on an arbitrary value
kind: enhancement
#450
opened Dec 3, 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
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
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
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)
#422
opened Nov 12, 2019 by
RustanLeino
"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
#406
opened Oct 28, 2019 by
robin-aws
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
ProTip!
Updated in the last three days: updated:>2024-06-22.