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

Exception in Translator.GetField 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: verifier Translation from Dafny to Boogie (translator)
#1316 opened Jul 19, 2021 by keyboardDrummer
Verification: can't reason with sequence prefix kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: verifier Translation from Dafny to Boogie (translator)
#1358 opened Aug 20, 2021 by sorawee
Detect meaningless modifies clauses on ghost methods kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#1350 opened Aug 13, 2021 by fpoli
1
rise4fun can't open now,is there any backup link? 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
#1344 opened Aug 10, 2021 by Aaron-clou
@robin-aws
1
Pretty printer - remove = from module imports with the same name kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: printer Pretty printer for Dafny's AST
#1343 opened Aug 6, 2021 by joscoh
Pretty printer spacing between decls is inconsistent kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: printer Pretty printer for Dafny's AST
#1342 opened Aug 6, 2021 by joscoh
sequence comprehensions are ugly 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
#1332 opened Jul 29, 2021 by jonhnet
12
Assumption failed from too deeply nested AST, resulting in a hard crash 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: resolver Resolution and typechecking
#1331 opened Jul 27, 2021 by sorawee
2
"Dependabot can't parse your Gemfile.lock" 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
#1329 opened Jul 26, 2021 by robin-aws
C# compilation error on a function returning complex sequence 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
#1326 opened Jul 25, 2021 by sorawee
Error: the type of this expression is underspecified kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: resolver Resolution and typechecking
#1325 opened Jul 25, 2021 by sorawee
1
type inference failure for datatype methods kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: resolver Resolution and typechecking
#1319 opened Jul 22, 2021 by jonhnet
Go compiler emits unused imports to extern modules kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: golang Dafny's transpiler to Go and its runtime part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag
#1317 opened Jul 19, 2021 by robin-aws
1
Grammar railroad diagram kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: documentation Dafny's reference manual, tutorial, and other materials part: parser First phase of Dafny's pipeline
#1244 opened Jun 6, 2021 by mingodad
@davidcok
9
CI only builds the reference manual on macos part: documentation Dafny's reference manual, tutorial, and other materials
#1315 opened Jul 19, 2021 by keyboardDrummer
@davidcok
1
Several tests don't pass on Windows 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 platform: windows Windows-specific issues
#1314 opened Jul 19, 2021 by keyboardDrummer
Lack of qualified type names makes error messages unclear area: error-reporting Clarity of the error reporting kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: resolver Resolution and typechecking
#1309 opened Jul 15, 2021 by joscoh
@davidcok
1
Dafny generates invalid Java code kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: java Dafny's Java transpiler and its runtime
#1297 opened Jul 13, 2021 by sorawee
Twostate greatest predicates 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
#1296 opened Jul 13, 2021 by fpoli
1
C++ compilation error on a datatype with a type parameter kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: c++ Dafny's C++ transpiler and its runtime
#1294 opened Jul 13, 2021 by fpoli
Type checking of match statements kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: resolver Resolution and typechecking
#1292 opened Jul 13, 2021 by typerSniper
Output issue in compile:3 for Java kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: java Dafny's Java transpiler and its runtime misc: cleanup Cleanups in the implementation or in corners of the language
#1291 opened Jul 13, 2021 by sorawee
4
Error reporting of wrong tuple types area: error-reporting Clarity of the error reporting kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: resolver Resolution and typechecking
#1283 opened Jul 9, 2021 by fpoli
1
Type of - inferred to be nat kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: resolver Resolution and typechecking
#1263 opened Jun 30, 2021 by RustanLeino
5
C++ support for unconstrained ints 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 misc: update Updates to a Dafny dependency part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag
#1259 opened Jun 22, 2021 by robin-aws
6
ProTip! Add no:assignee to see everything that’s not assigned.