Skip to content

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.

Sign up for GitHub

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

Clear current search query, filters, and sorts
1,021 Open 1,591 Closed
1,021 Open 1,591 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

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
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
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
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
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
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
Support calling ToString on an arbitrary value 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
#450 opened Dec 3, 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
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
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
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
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
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
Define backwards compatibility constraints for verification changes kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#609 opened May 1, 2020 by robin-aws
Cannot include opaque types in datatype definitions with higher-order functions kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#626 opened May 15, 2020 by danmatichuk
Unqualified reference to module constant from extern-ed class doesn't compile in Java 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: java Dafny's Java transpiler and its runtime part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag
#634 opened May 27, 2020 by robin-aws
Allow transpiled JS to be imported by external modules 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: js Dafny's JavaScript transpiler and its runtime part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag
#662 opened Jun 11, 2020 by lavaleri
Incorrect fuel parameter used in method override check kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: verifier Translation from Dafny to Boogie (translator)
#670 opened Jun 13, 2020 by RustanLeino
License copyright kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label misc: cleanup Cleanups in the implementation or in corners of the language
#738 opened Jul 20, 2020 by davidcok
@RustanLeino @anjjoshi
If compile:3 or 4 is chosen, warn if there is no Main kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag
#756 opened Jul 25, 2020 by davidcok
Consolidation of expect/assume/ensures/assert 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
#836 opened Aug 27, 2020 by davidcok
Implement refinement of newtype and datatypes kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#857 opened Sep 9, 2020 by davidcok
Resolution of names in dependency analysis kind: language development speed Slows down development of Dafny the language, flaky tests misc: cleanup Cleanups in the implementation or in corners of the language
#995 opened Dec 23, 2020 by davidcok
ProTip! Updated in the last three days: updated:>2024-06-22.