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
832 Open 919 Closed
832 Open 919 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

function transparency vs isolate-assertions vs split_here kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#5618 opened Jul 11, 2024 by hmijail
transparent function == verified multiple times? part: documentation Dafny's reference manual, tutorial, and other materials
#5617 opened Jul 11, 2024 by hmijail
Busy z3 process leaked kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#5616 opened Jul 11, 2024 by hmijail
Some verification iterations are successful, some fail? kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#5615 opened Jul 11, 2024 by hmijail
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
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
Unable to prove simple assertion when implementing a trait with a datatype kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#5604 opened Jul 5, 2024 by robin-aws
1
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
Havocs allow null arrays kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#5599 opened Jul 4, 2024 by anymeyer
1
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
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
[PRERELEASE REGRESSION] Dafny prerelease regression from smithy-lang/smithy-dafny
#5584 opened Jun 27, 2024 by dafny-lang-bot
13
Add by { ... } block to method calls 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
#5582 opened Jun 27, 2024 by keyboardDrummer
1
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
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
Malformed Boogie for if-then-else with non-reference traits kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#5570 opened Jun 24, 2024 by RustanLeino
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
Integrate MIRI as part of the CI to ensure no memory leak in the DafnyRuntimeRust
#5567 opened Jun 21, 2024 by MikaelMayer
[PRERELEASE REGRESSION] Dafny prerelease regression from aws/aws-cryptographic-material-providers-library
#5565 opened Jun 18, 2024 by aws-crypto-tools-ci-bot
22
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
7 tasks
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
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
1
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# backend: Multiset size overflow 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 priority: not yet Will reconsider working on this when we're looking for work
#5554 opened Jun 12, 2024 by khemichew
JavaScript and Go backend: Incorrect map cardinality 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 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
#5552 opened Jun 12, 2024 by khemichew
1
ProTip! Adding no:label will show everything without a label.