-
Notifications
You must be signed in to change notification settings - Fork 256
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
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
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
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
Add 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-paths
option
kind: enhancement
#5576
opened Jun 26, 2024 by
keyboardDrummer
Ensure the presence of a 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)
by {...}
block does not affect the SMT of the surrounding proofs
kind: enhancement
#5577
opened Jun 26, 2024 by
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
When 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
--isolate-assertions
is used, experiment with combining consecutive assertions into a single VC
kind: enhancement
#5602
opened Jul 5, 2024 by
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
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
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
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
transparent function == verified multiple times?
part: documentation
Dafny's reference manual, tutorial, and other materials
#5617
opened Jul 11, 2024 by
hmijail
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
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.