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
12 Open 7 Closed
12 Open 7 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

CLI tries to verify unmodified methods of refined types area: refinement Dafny's module-refinement machinery kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#5810 opened Oct 7, 2024 by erniecohen
2
function refinement broken area: refinement Dafny's module-refinement machinery 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 part: resolver Resolution and typechecking priority: next Will consider working on this after in progress work is done
#5366 opened Apr 25, 2024 by erniecohen
@robin-aws
2
Remove code for statement refinement area: refinement Dafny's module-refinement machinery difficulty: easy Issues that should take a few days at most to fix kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#3665 opened Mar 2, 2023 by davidcok
@davidcok
Refinement of submodules area: refinement Dafny's module-refinement machinery misc: language proposals Proposals for change to the language that go beyon simple enhancement requests
#2772 opened Sep 20, 2022 by davidcok
@RustanLeino
Missing refinement check for functions with bodies area: refinement Dafny's module-refinement machinery 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: next Will consider working on this after in progress work is done
#2557 opened Aug 5, 2022 by cpitclaudel
1
Default export set in abstract modules does not exist in refined module area: refinement Dafny's module-refinement machinery difficulty: easy Issues that should take a few days at most to fix has-workaround: yes There is a known workaround kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: resolver Resolution and typechecking status: needs-decision The cause of this issue is clear; the team needs to decide whether we want to work on it
#2356 opened Jul 4, 2022 by seebees
@davidcok
1
Allow importing a module as its interface area: refinement Dafny's module-refinement machinery kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: resolver Resolution and typechecking
#2250 opened Jun 14, 2022 by cpitclaudel
Error class 'ClassName' does not implement trait lemma when using abstract module area: refinement Dafny's module-refinement machinery part: resolver Resolution and typechecking
#2150 opened May 18, 2022 by seebees
4
Nontermination through module refinement area: refinement Dafny's module-refinement machinery 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 kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: resolver Resolution and typechecking priority: next Will consider working on this after in progress work is done
#2110 opened May 7, 2022 by cpitclaudel
1
Syntax for constant refinement could be improved area: refinement Dafny's module-refinement machinery 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
#2057 opened Apr 22, 2022 by cpitclaudel
Missing checks in statement superimposition part of refinement machinery area: refinement Dafny's module-refinement machinery 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 kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: resolver Resolution and typechecking priority: next Will consider working on this after in progress work is done
#2056 opened Apr 22, 2022 by cpitclaudel
enhancement: renaming area: refinement Dafny's module-refinement machinery 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
#1503 opened Oct 10, 2021 by erniecohen
ProTip! Exclude everything labeled bug with -label:bug.