-
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
Go compiler: invalid package name
has-workaround: yes
There is a known workaround
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
lang: golang
Dafny's transpiler to Go and its runtime
part: code-generation
Support for transpiling Dafny to another language. If relevant, add a `lang:` tag
#2682
opened Sep 1, 2022 by
sorawee
Stack overflow hard 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: boogie
Happens after passing the program to Boogie
#2588
opened Aug 13, 2022 by
sorawee
Encountered internal translation error
crash
Dafny crashes on this input, or generates malformed code that can not be executed
part: boogie
Happens after passing the program to Boogie
part: verifier
Translation from Dafny to Boogie (translator)
#2535
opened Aug 2, 2022 by
sorawee
Brittle verification
area: nonlinear arithmetic
Support for reasoning about nonlinear arithmetic
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
misc: brittleness
When Dafny sometimes proves something, and sometimes doesn't
status: needs-expert
Needs review by an expert on this part of the code
#2354
opened Jul 1, 2022 by
sorawee
Incorrect compile-time error reporting: NullReferenceException
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
priority: not yet
Will reconsider working on this when we're looking for work
#1438
opened Sep 15, 2021 by
sorawee
Java: compilation error on nested array
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: not yet
Will reconsider working on this when we're looking for work
#1414
opened Sep 3, 2021 by
sorawee
Problem with set of arrays
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
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: not yet
Will reconsider working on this when we're looking for work
#1402
opened Aug 28, 2021 by
sorawee
Java 8: compilation error from tuple + if expression
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: not yet
Will reconsider working on this when we're looking for work
#1397
opened Aug 27, 2021 by
sorawee
C#: compilation error on if expression of arrow type
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
part: resolver
Resolution and typechecking
priority: not yet
Will reconsider working on this when we're looking for work
#1396
opened Aug 27, 2021 by
sorawee
Verification: unknown length array should not be verified(?)
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
part: documentation
Dafny's reference manual, tutorial, and other materials
part: parser
First phase of Dafny's pipeline
part: resolver
Resolution and typechecking
priority: not yet
Will reconsider working on this when we're looking for work
#1395
opened Aug 27, 2021 by
sorawee
unexpected type error from multiset(.)
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
part: resolver
Resolution and typechecking
priority: not yet
Will reconsider working on this when we're looking for work
#1387
opened Aug 25, 2021 by
sorawee
Java 11: compile error from passing a set of map to a function method
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: not yet
Will reconsider working on this when we're looking for work
#1374
opened Aug 23, 2021 by
sorawee
Java: compilation error for map containing a function method
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: not yet
Will reconsider working on this when we're looking for work
#1372
opened Aug 22, 2021 by
sorawee
C#: compilation error for sequence comprehension
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
#1365
opened Aug 21, 2021 by
sorawee
Verification: failure from too large string argument
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
#1362
opened Aug 20, 2021 by
sorawee
Verification: can't reason with multiset intersection
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
#1360
opened Aug 20, 2021 by
sorawee
Verification: can't reason with sequence prefix
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
#1358
opened Aug 20, 2021 by
sorawee
Assumption failed from too deeply nested AST, resulting in a hard 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: resolver
Resolution and typechecking
priority: not yet
Will reconsider working on this when we're looking for work
#1331
opened Jul 27, 2021 by
sorawee
C# compilation error on a function returning complex sequence
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
lang: c#
Dafny's C# 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
#1326
opened Jul 25, 2021 by
sorawee
Error: the type of this expression is underspecified
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
part: resolver
Resolution and typechecking
priority: not yet
Will reconsider working on this when we're looking for work
#1325
opened Jul 25, 2021 by
sorawee
Dafny generates invalid Java code
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
#1297
opened Jul 13, 2021 by
sorawee
Output issue in compile:3 for Java
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
lang: java
Dafny's Java transpiler and its runtime
misc: cleanup
Cleanups in the implementation or in corners of the language
priority: not yet
Will reconsider working on this when we're looking for work
#1291
opened Jul 13, 2021 by
sorawee
ProTip!
Adding no:label will show everything without a label.