-
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
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
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
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
Flaky test: ConcurrentCompilationDoesNotBreakCaching
kind: language development speed
Slows down development of Dafny the language, flaky tests
priority: next
Will consider working on this after in progress work is done
#5515
opened May 31, 2024 by
MikaelMayer
Confusing type error due to missing path qualifier
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#5505
opened May 29, 2024 by
mschlaipfer
Integration tests getting really slow
kind: language development speed
Slows down development of Dafny the language, flaky tests
#5499
opened May 28, 2024 by
robin-aws
Incorrect multiplication in Dafny: Show Counterexample
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
part: counterexamples
Counterexample generation
#5490
opened May 25, 2024 by
cdstanford
Previous Next
ProTip!
Type g i on any issue or pull request to go back to the issue listing page.