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
22 Open 12 Closed
22 Open 12 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

Go compiler: invalid package name has-workaround: yes There is a known workaround 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
#2682 opened Sep 1, 2022 by sorawee
Stack overflow 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: boogie Happens after passing the program to Boogie
#2588 opened Aug 13, 2022 by sorawee
1
Encountered internal translation error crash Dafny crashes on this input, or generates malformed code that can not be executed part: boogie Happens after passing the program to Boogie part: verifier Translation from Dafny to Boogie (translator)
#2535 opened Aug 2, 2022 by sorawee
3
Brittle verification area: nonlinear arithmetic Support for reasoning about nonlinear arithmetic kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny misc: brittleness When Dafny sometimes proves something, and sometimes doesn't status: needs-expert Needs review by an expert on this part of the code
#2354 opened Jul 1, 2022 by sorawee
2
Incorrect compile-time error reporting: NullReferenceException 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 priority: not yet Will reconsider working on this when we're looking for work
#1438 opened Sep 15, 2021 by sorawee
Java: compilation error on nested array kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label 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 priority: not yet Will reconsider working on this when we're looking for work
#1414 opened Sep 3, 2021 by sorawee
3
Problem with set of arrays kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: java Dafny's Java transpiler and its runtime 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 priority: not yet Will reconsider working on this when we're looking for work
#1402 opened Aug 28, 2021 by sorawee
Java 8: compilation error from tuple + if expression kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label 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 priority: not yet Will reconsider working on this when we're looking for work
#1397 opened Aug 27, 2021 by sorawee
1
C#: compilation error on if expression of arrow type kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: resolver Resolution and typechecking priority: not yet Will reconsider working on this when we're looking for work
#1396 opened Aug 27, 2021 by sorawee
Verification: unknown length array should not be verified(?) kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: documentation Dafny's reference manual, tutorial, and other materials part: parser First phase of Dafny's pipeline part: resolver Resolution and typechecking priority: not yet Will reconsider working on this when we're looking for work
#1395 opened Aug 27, 2021 by sorawee
1
unexpected type error from multiset(.) kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: resolver Resolution and typechecking priority: not yet Will reconsider working on this when we're looking for work
#1387 opened Aug 25, 2021 by sorawee
1
Java 11: compile error from passing a set of map to a function method kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label 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 priority: not yet Will reconsider working on this when we're looking for work
#1374 opened Aug 23, 2021 by sorawee
2
Java: compilation error for map containing a function method kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label 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 priority: not yet Will reconsider working on this when we're looking for work
#1372 opened Aug 22, 2021 by sorawee
1
C#: compilation error for sequence comprehension kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: c# Dafny's C# transpiler and its runtime priority: not yet Will reconsider working on this when we're looking for work
#1365 opened Aug 21, 2021 by sorawee
Verification: failure from too large string argument 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
#1362 opened Aug 20, 2021 by sorawee
@RustanLeino
2
Verification: can't reason with multiset intersection 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
#1360 opened Aug 20, 2021 by sorawee
2
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) priority: not yet Will reconsider working on this when we're looking for work
#1358 opened Aug 20, 2021 by sorawee
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 priority: not yet Will reconsider working on this when we're looking for work
#1331 opened Jul 27, 2021 by sorawee
2
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 priority: not yet Will reconsider working on this when we're looking for work
#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 priority: not yet Will reconsider working on this when we're looking for work
#1325 opened Jul 25, 2021 by sorawee
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 priority: not yet Will reconsider working on this when we're looking for work
#1297 opened Jul 13, 2021 by sorawee
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 priority: not yet Will reconsider working on this when we're looking for work
#1291 opened Jul 13, 2021 by sorawee
4
ProTip! Adding no:label will show everything without a label.