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
54 Open 142 Closed
54 Open 142 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

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
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
1
@RustanLeino
Base type throws off witness checking 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 part: verifier Translation from Dafny to Boogie (translator)
#5520 opened Jun 3, 2024 by RustanLeino
1
@RustanLeino
Precondition of merge sort too strong 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: next Will consider working on this after in progress work is done
#5286 opened Apr 1, 2024 by RustanLeino
@robin-aws
Compilation of :| assume omitted 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 part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag priority: next Will consider working on this after in progress work is done
#5166 opened Mar 8, 2024 by RustanLeino
2
Add X-is-a-statement-not-an-expression error messages area: error-reporting Clarity of the error reporting kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#5047 opened Feb 2, 2024 by RustanLeino
Don't allow two-state predicates in one-state lemmas kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#4723 opened Oct 27, 2023 by RustanLeino
1
Module name "Module" cannot be used with Java 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 lang: java Dafny's Java transpiler and its runtime priority: next Will consider working on this after in progress work is done
#4256 opened Jul 6, 2023 by RustanLeino
Universal elimination not working for opaque functions kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#3881 opened Apr 18, 2023 by RustanLeino
1
Type test for char kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#3814 opened Mar 28, 2023 by RustanLeino
2
Extend auto-ghost to let/assign-such-that kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: resolver Resolution and typechecking
#3695 opened Mar 6, 2023 by RustanLeino
2
Imported trait exported as provides should not be usable in extends crash Dafny crashes on this input, or generates malformed code that can not be executed during 1: program development Bad error message or documentation; IDE bug; crash compiling invalid program kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: resolver Resolution and typechecking
#3632 opened Feb 24, 2023 by RustanLeino
Consistency in array-length limits kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag
#3212 opened Dec 16, 2022 by RustanLeino
@robin-aws
3
[Feature request]: Reduce "file contains no code" messages difficulty: good-first-issue Good first issues
#3090 opened Nov 21, 2022 by RustanLeino
1
[Bug]: Name clashes in compilation of datatypes during 2: compilation of correct program Dafny rejects a valid program during compilation invalid translated code The compiler generates invalid code, making the the target language infrastructure crash lang: c# Dafny's C# transpiler and its runtime lang: golang Dafny's transpiler to Go and its runtime lang: java Dafny's Java transpiler and its runtime
#3068 opened Nov 17, 2022 by RustanLeino
1
[Bug]: Default values of nested arrays broken in Java crash Dafny crashes on this input, or generates malformed code that can not be executed during 2: compilation of correct program Dafny rejects a valid program during compilation invalid translated code The compiler generates invalid code, making the the target language infrastructure crash kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: java Dafny's Java transpiler and its runtime part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag testing-method: uniform-backend-testing Issues found by ensuring uniform testing across backends
#3055 opened Nov 14, 2022 by RustanLeino
@alex-chew
Constant fields depending on non-initialized fields should not be usable in first-phase construction 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 introduced: pre-2012 part: resolver Resolution and typechecking priority: not yet Will reconsider working on this when we're looking for work
#2727 opened Sep 12, 2022 by RustanLeino
1
@MikaelMayer
10
Change of argument syntax for reveal statements breaking-change Any change that will cause existing Dafny codebases to break (excluding verification instability) kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#2689 opened Sep 2, 2022 by RustanLeino
4
Sequence membership versus sequence indexing kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: verifier Translation from Dafny to Boogie (translator)
#2644 opened Aug 25, 2022 by RustanLeino
1
Statement starting location is off difficulty: good-first-issue Good first issues part: parser First phase of Dafny's pipeline
#2483 opened Jul 22, 2022 by RustanLeino
1
Use verification caching in IDE part: language server Support for LSP in Dafny (server part; client is in ide-vscode repo)
#2468 opened Jul 21, 2022 by RustanLeino
3
Missing cyclicity check for inferred newtype base types crash Dafny crashes on this input, or generates malformed code that can not be executed kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: resolver Resolution and typechecking status: postponed The team is not planning to work on this in the near future
#2134 opened May 12, 2022 by RustanLeino
1
An opaque type should only be export-provided part: resolver Resolution and typechecking
#2098 opened May 5, 2022 by RustanLeino
Empty type of let variable assumed before binding 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 introduced: v3.0.0 kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: verifier Translation from Dafny to Boogie (translator) priority: next Will consider working on this after in progress work is done status: needs-info Issue requires more information from poster
#1958 opened Apr 1, 2022 by RustanLeino
1
ProTip! Updated in the last three days: updated:>2024-06-22.