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
55 Open 142 Closed
55 Open 142 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

Hint when tuples are used in decreases clauses difficulty: good-first-issue Good first issues kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#1517 opened Oct 15, 2021 by RustanLeino
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
2
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
Incorrect printing of unsigned integers in Java lang: java Dafny's Java transpiler and its runtime
#800 opened Aug 15, 2020 by RustanLeino
1
Errors from malformed Boogie should be marked as internal error kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: verifier Translation from Dafny to Boogie (translator)
#858 opened Sep 10, 2020 by RustanLeino
2
Name conflicts in target code kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: c# Dafny's C# transpiler and its runtime lang: golang Dafny's transpiler to Go and its runtime 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
#1103 opened Feb 5, 2021 by RustanLeino
Using Java keyword as filename causes 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 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
#1104 opened Feb 5, 2021 by RustanLeino
Some function allocatedness test are suppressed during 3: execution of incorrect program An bug in the verifier that allows Dafny to run a program that does not correctly implement its spec introduced: 2.0.0 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
#1120 opened Feb 16, 2021 by RustanLeino
1
Duplicate :extern name causes 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: verifier Translation from Dafny to Boogie (translator)
#1170 opened Apr 3, 2021 by RustanLeino
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
Info tool tips repeated during export consistency checks kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: resolver Resolution and typechecking
#1433 opened Sep 13, 2021 by RustanLeino
Support for :- assert/assume/expect in expressions kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#1434 opened Sep 14, 2021 by RustanLeino
1
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
Solver does not abide by /timeLimit kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: verifier Translation from Dafny to Boogie (translator)
#1457 opened Sep 23, 2021 by RustanLeino
Unary minus on bitvector type synonym causes crash crash Dafny crashes on this input, or generates malformed code that can not be executed difficulty: good-first-issue Good first issues part: verifier Translation from Dafny to Boogie (translator)
#1533 opened Oct 22, 2021 by RustanLeino
1
Type-test binding not compiled correctly during 4: bad execution of correct program A bug in the Dafny compiler that causes a correct Dafny program to execute incorrectly kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: c# Dafny's C# transpiler and its runtime lang: c++ Dafny's C++ transpiler and its runtime lang: golang Dafny's transpiler to Go and its runtime 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: next Will consider working on this after in progress work is done
#1541 opened Oct 25, 2021 by RustanLeino
1
lambda expression passed to extreme lemma causes 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: verifier Translation from Dafny to Boogie (translator)
#1542 opened Oct 26, 2021 by RustanLeino
Trigger discovery not applied to type constraints and witnesses difficulty: good-first-issue Good first issues part: resolver Resolution and typechecking
#1544 opened Oct 26, 2021 by RustanLeino
Function values are not checked for ghost parameters kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: resolver Resolution and typechecking
#1567 opened Nov 5, 2021 by RustanLeino
Termination of dynamic dispatch kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: verifier Translation from Dafny to Boogie (translator)
#1588 opened Nov 13, 2021 by RustanLeino
14
Enhanced range and index expressions kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#1589 opened Nov 15, 2021 by RustanLeino
1
Fine-grained frame expressions for arrays kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#1590 opened Nov 15, 2021 by RustanLeino
Warning when constructor name is used as variable in match area: error-reporting Clarity of the error reporting kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#1600 opened Nov 19, 2021 by RustanLeino
1
@tobiaj10
4
Include subtypes in case patterns 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
#1715 opened Jan 14, 2022 by RustanLeino
14
Bad related error location for inlined conjunct area: error-reporting Clarity of the error reporting kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#5586 opened Jun 28, 2024 by RustanLeino
1
@RustanLeino
ProTip! Find all open issues with in progress development work with linked:pr.