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,020 Open 1,592 Closed
1,020 Open 1,592 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

Remove the use of Boogie's XML output misc: cleanup Cleanups in the implementation or in corners of the language
#1950 by atomb was closed Aug 18, 2022
1
@atomb
🎉 1
C++ backend for Dafny 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
#563 by parno was closed Jul 22, 2020
@parno
6 🎉 1
Fatal exception in parser (?)
#3 by plaidfinch was closed Jun 30, 2016
@qunyanm
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
@qunyanm
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
@qunyanm
1
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
@qunyanm
3
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
2
missing "ghost" keywords when printing expressions in methods
#8 by danmatichuk was closed Jul 12, 2016
@danmatichuk
Trigger loop introduced by the new fuel-based reveal
#9 by parno was closed Jul 16, 2016
@parno
/trace output is less helpful than it could be due to buffering
#10 by 0xabu was closed Jul 15, 2016
5
opaque and literals
#11 by Chris-Hawblitzel was closed Sep 16, 2016
@parno
1
Dafny's occurs-check for type synonyms can be tricked
#12 by plaidfinch was closed Aug 5, 2016
@plaidfinch
Deep function causes Dafny Visual Studio extension to hang
#14 by jaylorch was closed Jul 26, 2016
@jaylorch
Dafny crash in Translator.FuelSetting.GetFunctionFuel
#1 by jaylorch was closed Jun 24, 2016
@qunyanm
3
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
@plaidfinch
5
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
Helpers.unsignedLongToBigInteger removed from Java runtime release-blocker Must be resolved before the next release
#5553 by robin-aws was closed Jun 17, 2024
1
@robin-aws
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
1
@jtristan @RustanLeino
5
opaque leaked through consequence axiom
#20 by Chris-Hawblitzel was closed Sep 2, 2016
@parno
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
@qunyanm
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
@qunyanm
3
Dafny VS extension crashes when including lengthy files
#24 by parno was closed Sep 2, 2016
@parno
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
3
Assertion failure in CompatibleDecreasesTypes with bv32 type
#26 by 0xabu was closed Oct 6, 2016
@qunyanm
Compilation Error: generates duplicate local variable declarations
#15 by laurejt was closed Jul 26, 2016
@laurejt
ProTip! Follow long discussions with comments:>50.