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,081 Open 1,634 Closed
1,081 Open 1,634 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

Potential enhancement: array initialisation that is incompatible with declared size 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 kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny priority: not yet Will reconsider working on this when we're looking for work
#5556 opened Jun 12, 2024 by khemichew
C# and Go Backends: Incorrect finite map semantics 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 kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: golang Dafny's transpiler to Go and its runtime lang: js Dafny's JavaScript transpiler and its runtime priority: not yet Will reconsider working on this when we're looking for work
#5557 opened Jun 12, 2024 by khemichew
2
Make the Rust compiler run on nightly once it passes all tests part: ci Issue is with Dafny's CI infrastructure part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag priority: now Will work on this now
#5560 opened Jun 14, 2024 by MikaelMayer
Dafny-to-Rust code generator part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag priority: now Will work on this now
#5561 opened Jun 14, 2024 by MikaelMayer
5 of 16 tasks
[PRERELEASE REGRESSION] Dafny prerelease regression from aws/aws-cryptographic-material-providers-library
#5565 opened Jun 18, 2024 by aws-crypto-tools-ci-bot
86
Integrate MIRI as part of the CI to ensure no memory leak in the DafnyRuntimeRust
#5567 opened Jun 21, 2024 by MikaelMayer
Ordering problem in Python code generator kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: python Dafny's Python transpiler and its runtime part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag
#5569 opened Jun 24, 2024 by RustanLeino
Malformed Boogie for if-then-else with non-reference traits difficulty: easy Issues that should take a few days at most to fix during 2: compilation of correct program Dafny rejects a valid program during compilation kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label priority: not yet Will reconsider working on this when we're looking for work
#5570 opened Jun 24, 2024 by RustanLeino
Enable hiding of functions to an extend that it could make opaque obsolete
#5575 opened Jun 25, 2024 by keyboardDrummer
@keyboardDrummer
1
Add --isolate-paths option 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)
#5576 opened Jun 26, 2024 by keyboardDrummer
Ensure the presence of a by {...} block does not affect the SMT of the surrounding proofs 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)
#5577 opened Jun 26, 2024 by keyboardDrummer
@keyboardDrummer
No line/column information reported on some type errors when a datatype extends a trait kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#5590 opened Jul 1, 2024 by dschoepe
Malformed DafnyPrelude causes silent failure and reports success area: error-reporting Clarity of the error reporting 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 kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#5592 opened Jul 1, 2024 by RustanLeino
Havocs allow null arrays 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)
#5599 opened Jul 4, 2024 by anymeyer
@keyboardDrummer
3
When --isolate-assertions is used, experiment with combining consecutive assertions into a single VC 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
#5602 opened Jul 5, 2024 by keyboardDrummer
@keyboardDrummer
Unable to prove value of map.Values for simple maps kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#5603 opened Jul 5, 2024 by benreynwar
Unable to prove simple assertion when implementing a trait with a datatype during 2: compilation of correct program Dafny rejects a valid program during compilation incompleteness Things that Dafny should be able to prove, but can't kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label priority: not yet Will reconsider working on this when we're looking for work
#5604 opened Jul 5, 2024 by robin-aws
1
IDE regression: Flickering of resolution items kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: language server Support for LSP in Dafny (server part; client is in ide-vscode repo)
#5605 opened Jul 5, 2024 by MikaelMayer
@keyboardDrummer
1
Test generation cannot find witness for type nat kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: test generation Relates to the dafny generate-tests command
#5607 opened Jul 8, 2024 by stefan-aws
1
Test generation violates preconditions kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: test generation Relates to the dafny generate-tests command
#5612 opened Jul 10, 2024 by stefan-aws
Busy z3 process leaked kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#5616 opened Jul 11, 2024 by hmijail
1
transparent function == verified multiple times? part: documentation Dafny's reference manual, tutorial, and other materials
#5617 opened Jul 11, 2024 by hmijail
1
function transparency vs isolate-assertions vs split_here misc: question Questions about Dafny's implementation. For beginner questions use "discussions" or StackOverflow
#5618 opened Jul 11, 2024 by hmijail
4
Flaky test: ChangedImportAffectsExport kind: language development speed Slows down development of Dafny the language, flaky tests
#5619 opened Jul 11, 2024 by MikaelMayer
Better path error reporting 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: verifier Translation from Dafny to Boogie (translator)
#5628 opened Jul 16, 2024 by keyboardDrummer
ProTip! Type g i on any issue or pull request to go back to the issue listing page.