-
Notifications
You must be signed in to change notification settings - Fork 261
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.
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
Author
Label
Projects
Milestones
Assignee
Sort
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
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
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
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 Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
dafny audit
kind: bug
#5821
opened Oct 9, 2024 by
atomb
When Dafny verification runs out of time or tick resources, automatically rerun verification with 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)
{:isolate_assertions}
kind: enhancement
#5819
opened Oct 9, 2024 by
keyboardDrummer
Introduce an 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
{:isolate_branches}
attribute that can be used at the method level
kind: enhancement
#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
No Counterexample states generated when using the attribute 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
{:isolate_assertions}
kind: bug
#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
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
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
Previous Next
ProTip!
Type g i on any issue or pull request to go back to the issue listing page.