-
Notifications
You must be signed in to change notification settings - Fork 254
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
Enable hiding of functions to an extend that it could make opaque obsolete
#5575
opened Jun 25, 2024 by
keyboardDrummer
Disjunctive pattern matching not correctly handled
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
#5572
opened Jun 25, 2024 by
MikaelMayer
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
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
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
Dafny generated code not necessarily backwards compatible with code generated by older Dafny versions
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
priority: now
Will work on this now
release-blocker
Must be resolved before the next release
#5555
opened Jun 12, 2024 by
robin-aws
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
Flaky test: Unspecified
kind: language development speed
Slows down development of Dafny the language, flaky tests
part: ci
Issue is with Dafny's CI infrastructure
priority: not yet
Will reconsider working on this when we're looking for work
#5551
opened Jun 11, 2024 by
MikaelMayer
Named ensure clause
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
part: language definition
Relating to the Dafny language definition itself
priority: not yet
Will reconsider working on this when we're looking for work
#5544
opened Jun 7, 2024 by
keyboardDrummer
can't label assumptions
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
part: language definition
Relating to the Dafny language definition itself
priority: not yet
Will reconsider working on this when we're looking for work
#5540
opened Jun 7, 2024 by
kjx
can't label forall-ensuring statement
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
part: language definition
Relating to the Dafny language definition itself
priority: not yet
Will reconsider working on this when we're looking for work
#5539
opened Jun 7, 2024 by
kjx
Unstable CLI test Slows down development of Dafny the language, flaky tests
part: ci
Issue is with Dafny's CI infrastructure
priority: not yet
Will reconsider working on this when we're looking for work
git-issues/git-issue-697j.dfy
, related to Rust backend
kind: language development speed
#5537
opened Jun 6, 2024 by
keyboardDrummer
Costless by clause in Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
part: boogie
Happens after passing the program to Boogie
priority: not yet
Will reconsider working on this when we're looking for work
assert .. by { }
when using --isolate-assertions
kind: enhancement
#5536
opened Jun 6, 2024 by
keyboardDrummer
Verification hang apparently caused by Std import
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
part: standard libraries
Standard libraries packaged in the Dafny distribution
priority: not yet
Will reconsider working on this when we're looking for work
#5534
opened Jun 6, 2024 by
nverhaaren
Issue with multi-backend-testing
kind: language development speed
Slows down development of Dafny the language, flaky tests
priority: not yet
Will reconsider working on this when we're looking for work
#5533
opened Jun 5, 2024 by
MikaelMayer
Bad encoding for Dafny rejects a valid program during compilation
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
lang: java
Dafny's Java transpiler and its runtime
priority: not yet
Will reconsider working on this when we're looking for work
this
in tail recursive functions when compiling to Java
during 2: compilation of correct program
#5532
opened Jun 5, 2024 by
fabiomadge
assertion of map values fails when same postcondition succeeds (or if preceded by Keys assertion)
incompleteness
Things that Dafny should be able to prove, but can't
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
part: verifier
Translation from Dafny to Boogie (translator)
priority: not yet
Will reconsider working on this when we're looking for work
#5527
opened Jun 5, 2024 by
kjx
Verification ignores resource limits
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
part: z3
Issue is in Z3
priority: not yet
Will reconsider working on this when we're looking for work
#5525
opened Jun 4, 2024 by
hmijail
Constraint-less newtypes assumed to be nonempty
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
#5521
opened Jun 3, 2024 by
RustanLeino
Previous Next
ProTip!
What’s not been updated in a month: updated:<2024-05-25.