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

1,104 Open 1,653 Closed
1,104 Open 1,653 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

Cache constant RHS value evaluation at runtime kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#5861 opened Oct 25, 2024 by robin-aws
Optimization to use slice_usize in Rust kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#5857 opened Oct 24, 2024 by ajewellamz
1
truncate!(int!(256)) fails to simplify in Rust kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#5856 opened Oct 24, 2024 by ajewellamz
Abstract import of concrete module is allowed, produces invalid target code invalid translated code The compiler generates invalid code, making the the target language infrastructure crash kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#5854 opened Oct 23, 2024 by ssomayyajula
AccessViolationException durring verification kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#5853 opened Oct 23, 2024 by seebees
Dafny-to-Rust Performance improvement: access sequence by usize, not int
#5850 opened Oct 22, 2024 by MikaelMayer
Java versions supported? kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#5849 opened Oct 22, 2024 by damienstanton
Type parameter Equality wrongly inferred kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#5844 opened Oct 18, 2024 by MikaelMayer
Trait postcondition ignored kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#5840 opened Oct 17, 2024 by jaylorch
Warnings raised from
#5838 opened Oct 16, 2024 by seebees
4
Extern names (inconsistently) escaped to avoid target language keywords kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#5836 opened Oct 16, 2024 by robin-aws
bitvector rotation operations sometimes reported nonexisting by incremental resolver kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#5830 opened Oct 12, 2024 by erniecohen
newtype based on bv64 crashes resolver kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#5829 opened Oct 12, 2024 by erniecohen
1
missing bitvector operators part: documentation Dafny's reference manual, tutorial, and other materials
#5828 opened Oct 12, 2024 by erniecohen
Feature/Bug: Ensures clauses of bodiless functions should have reads checks difficulty: good-first-issue Good first issues part: verifier Translation from Dafny to Boogie (translator)
#5822 opened Oct 9, 2024 by MikaelMayer
Incorrect warning about trait method with no body from dafny audit kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#5821 opened Oct 9, 2024 by atomb
When Dafny verification runs out of time or tick resources, automatically rerun verification with {:isolate_assertions} 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 part: verifier Translation from Dafny to Boogie (translator)
#5819 opened Oct 9, 2024 by keyboardDrummer
Introducing Dafny Guru on Gurubase.io
#5818 opened Oct 9, 2024 by kursataktas
Introduce an {:isolate_branches} attribute that can be used at the method level 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 priority: not yet Will reconsider working on this when we're looking for work
#5817 opened Oct 9, 2024 by keyboardDrummer
CLI tries to verify unmodified methods of refined types kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#5810 opened Oct 7, 2024 by erniecohen
1
No Counterexample states generated when using the attribute {:isolate_assertions} kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label misc: brittleness When Dafny sometimes proves something, and sometimes doesn't part: verifier Translation from Dafny to Boogie (translator) priority: next Will consider working on this after in progress work is done
#5806 opened Oct 3, 2024 by TomSMaier
Resource Limit hides subsequent assertion failures within a method kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label misc: brittleness When Dafny sometimes proves something, and sometimes doesn't part: verifier Translation from Dafny to Boogie (translator) priority: next Will consider working on this after in progress work is done
#5805 opened Oct 3, 2024 by TomSMaier
1
Flaky test on Windows: OpeningDocumentWithTimeoutReportsTimeoutDiagnostic kind: language development speed Slows down development of Dafny the language, flaky tests
#5798 opened Sep 27, 2024 by MikaelMayer
At-attributes - new language feature kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#5795 opened Sep 26, 2024 by MikaelMayer
1
Dafny --no-verify doesn't speed up compilation of already verified programs kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#5794 opened Sep 25, 2024 by BeamRaceMuppet
@keyboardDrummer
1
ProTip! Type g i on any issue or pull request to go back to the issue listing page.