-
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
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
Improve set/map implementation for Go
lang: golang
Dafny's transpiler to Go and its runtime
part: runtime
Happens in Dafny's runtime (Add a `lang` tag if relevant)
#1897
opened Mar 11, 2022 by
RustanLeino
Support monomorphization of collection types in Dafny runtimes
lang: golang
Dafny's transpiler to Go and its runtime
lang: js
Dafny's JavaScript transpiler and its runtime
part: runtime
Happens in Dafny's runtime (Add a `lang` tag if relevant)
#1896
opened Mar 11, 2022 by
RustanLeino
match-optimization removes expressions before they are verified
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
part: verifier
Translation from Dafny to Boogie (translator)
#1880
opened Mar 2, 2022 by
RustanLeino
for loop turns into illegal decreases-* in iterator
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
part: verifier
Translation from Dafny to Boogie (translator)
#1793
opened Feb 7, 2022 by
RustanLeino
Include subtypes in case patterns
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
#1715
opened Jan 14, 2022 by
RustanLeino
Warning when constructor name is used as variable in match
area: error-reporting
Clarity of the error reporting
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#1600
opened Nov 19, 2021 by
RustanLeino
Fine-grained frame expressions for arrays
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#1590
opened Nov 15, 2021 by
RustanLeino
Enhanced range and index expressions
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#1589
opened Nov 15, 2021 by
RustanLeino
Termination of dynamic dispatch
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
part: verifier
Translation from Dafny to Boogie (translator)
#1588
opened Nov 13, 2021 by
RustanLeino
Function values are not checked for ghost parameters
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
part: resolver
Resolution and typechecking
#1567
opened Nov 5, 2021 by
RustanLeino
Trigger discovery not applied to type constraints and witnesses
difficulty: good-first-issue
Good first issues
part: resolver
Resolution and typechecking
#1544
opened Oct 26, 2021 by
RustanLeino
lambda expression passed to extreme lemma causes crash
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: verifier
Translation from Dafny to Boogie (translator)
#1542
opened Oct 26, 2021 by
RustanLeino
Type-test binding not compiled correctly
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
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
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: next
Will consider working on this after in progress work is done
#1541
opened Oct 25, 2021 by
RustanLeino
Unary minus on bitvector type synonym causes crash
crash
Dafny crashes on this input, or generates malformed code that can not be executed
difficulty: good-first-issue
Good first issues
part: verifier
Translation from Dafny to Boogie (translator)
#1533
opened Oct 22, 2021 by
RustanLeino
Hint when tuples are used in decreases clauses
difficulty: good-first-issue
Good first issues
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#1517
opened Oct 15, 2021 by
RustanLeino
Solver does not abide by /timeLimit
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
part: verifier
Translation from Dafny to Boogie (translator)
#1457
opened Sep 23, 2021 by
RustanLeino
Support for Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
:- assert/assume/expect
in expressions
kind: enhancement
#1434
opened Sep 14, 2021 by
RustanLeino
Info tool tips repeated during export consistency checks
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
part: resolver
Resolution and typechecking
#1433
opened Sep 13, 2021 by
RustanLeino
Type of - inferred to be nat
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
part: resolver
Resolution and typechecking
#1263
opened Jun 30, 2021 by
RustanLeino
Duplicate :extern name causes crash
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: verifier
Translation from Dafny to Boogie (translator)
#1170
opened Apr 3, 2021 by
RustanLeino
Some function allocatedness test are suppressed
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: 2.0.0
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
part: verifier
Translation from Dafny to Boogie (translator)
priority: not yet
Will reconsider working on this when we're looking for work
#1120
opened Feb 16, 2021 by
RustanLeino
Using Java keyword as filename causes crash
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
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
#1104
opened Feb 5, 2021 by
RustanLeino
Name conflicts in target code
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
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
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
#1103
opened Feb 5, 2021 by
RustanLeino
Errors from malformed Boogie should be marked as internal error
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
part: verifier
Translation from Dafny to Boogie (translator)
#858
opened Sep 10, 2020 by
RustanLeino
ProTip!
What’s not been updated in a month: updated:<2024-06-11.