-
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
Add dedicated content on determinism and methods vs. functions to the reference manual
part: documentation
Dafny's reference manual, tutorial, and other materials
priority: next
Will consider working on this after in progress work is done
#5372
opened Apr 26, 2024 by
robin-aws
Crash on reads with different datatype ordering
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
priority: next
Will consider working on this after in progress work is done
#5232
opened Mar 21, 2024 by
txiang61
Empty type initialization leads to proving false
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)
priority: next
Will consider working on this after in progress work is done
#5136
opened Feb 29, 2024 by
MikaelMayer
Disambiguation priority not preserved when importing modules
during 4: bad execution of correct program
A bug in the Dafny compiler that causes a correct Dafny program to execute incorrectly
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
priority: next
Will consider working on this after in progress work is done
#4364
opened Jul 31, 2023 by
xumingkuan
Java Build Name Clash
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
priority: next
Will consider working on this after in progress work is done
#4336
opened Jul 25, 2023 by
DavePearce
Quantifying over map.Keys has quadratic runtime in Java
area: performance
Performance issues
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
priority: next
Will consider working on this after in progress work is done
#4010
opened May 15, 2023 by
robin-aws
ProTip!
Type g p on any issue or pull request to go back to the pull request listing page.