Ecosyste.ms: Issues
An open API service for providing issue and pull request metadata for open source projects.
GitHub / dafny-lang/dafny issues and pull requests
#3872 - invariants as members
Issue -
State: open - Opened by erniecohen over 1 year ago
- 1 comment
Labels: kind: enhancement
#3871 - Incorrect cardinality of set and multiset<array> - Java Miscompilation error
Issue -
State: closed - Opened by Dilan-s over 1 year ago
- 3 comments
Labels: kind: bug, lang: java, severity: soundness (wrong result)
#3870 - Some auditor adjustments
Pull Request -
State: closed - Opened by atomb over 1 year ago
#3868 - Nested LetExpr chain compiles to tons of nested Java lambdas, which javac chokes on
Issue -
State: open - Opened by robin-aws over 1 year ago
- 3 comments
Labels: kind: bug, lang: java
#3865 - [Test Generation] Control inlining using method annotations
Pull Request -
State: closed - Opened by Dargones over 1 year ago
- 6 comments
#3858 - Remove IncludeToken as prep for caching parsing
Pull Request -
State: closed - Opened by keyboardDrummer over 1 year ago
#3855 - {:ignore} attribute crashes dafny with a null pointer error
Issue -
State: closed - Opened by kjx over 1 year ago
- 3 comments
Labels: kind: bug, part: resolver, severity: crash
#3854 - Java back end: incompatible type error (crash)
Issue -
State: open - Opened by alex-usher over 1 year ago
- 3 comments
Labels: kind: bug, part: code-generation, lang: java, severity: crash, severity: invalid code
#3854 - Java back end: incompatible type error (crash)
Issue -
State: open - Opened by alex-usher over 1 year ago
- 3 comments
Labels: kind: bug, part: code-generation, lang: java, severity: crash, severity: invalid code
#3852 - Update test to match new output from Go compiler
Pull Request -
State: closed - Opened by atomb over 1 year ago
Labels: run-deep-tests
#3849 - Creating a dafny doc tool
Pull Request -
State: open - Opened by davidcok over 1 year ago
- 3 comments
Labels: run-deep-tests
#3848 - Enable configuring the Dafny version in the Dafny project file
Issue -
State: open - Opened by keyboardDrummer over 1 year ago
- 5 comments
Labels: kind: enhancement, status: needs-approval, part: CLI
#3845 - Run the inline out variable declaration refactoring, across the codebase
Pull Request -
State: closed - Opened by keyboardDrummer over 1 year ago
#3841 - [Counterexamples] Support constant fields
Pull Request -
State: closed - Opened by Dargones over 1 year ago
- 2 comments
#3822 - Missing cyclicity checks cause hang
Issue -
State: closed - Opened by RustanLeino over 1 year ago
- 1 comment
Labels: kind: bug, part: resolver
#3818 - Support generating test running code when using `dafny translate`
Issue -
State: closed - Opened by keyboardDrummer over 1 year ago
- 4 comments
Labels: kind: enhancement
#3815 - `dafny run` writes both Dafny and user program output to stdout
Issue -
State: open - Opened by cdisselkoen over 1 year ago
- 2 comments
Labels: kind: enhancement
#3801 - Retrying the fix to issue 2959
Pull Request -
State: closed - Opened by davidcok over 1 year ago
Labels: run-deep-tests
#3792 - Crash during translation
Issue -
State: closed - Opened by MikaelMayer over 1 year ago
- 1 comment
Labels: kind: bug, part: verifier
#3791 - Adding coverage from doc tests
Pull Request -
State: closed - Opened by davidcok over 1 year ago
- 1 comment
#3787 - Using quicktest in release-brew
Pull Request -
State: closed - Opened by davidcok over 1 year ago
#3780 - Add documentation regarding type characteristics on type definitions (not just type parameters)
Issue -
State: closed - Opened by davidcok over 1 year ago
Labels: part: documentation
#3777 - Add number of assumptions found to output of `dafny audit`
Issue -
State: closed - Opened by atomb over 1 year ago
- 2 comments
Labels: kind: enhancement, area: error-reporting, difficulty: easy
#3769 - Exposing --output and --spill-translation in dafny test, per Issue 3612
Pull Request -
State: closed - Opened by davidcok over 1 year ago
- 1 comment
#3767 - Testing RM building on ubuntu
Pull Request -
State: closed - Opened by davidcok over 1 year ago
#3766 - Recursive datatype has incorrectly initialized Java type descriptor
Issue -
State: closed - Opened by alex-chew over 1 year ago
- 3 comments
Labels: kind: bug, part: code-generation, lang: java, severity: has-workaround, severity: soundness (crash)
#3757 - Crash on bad input
Issue -
State: closed - Opened by davidcok over 1 year ago
Labels: kind: bug, part: parser
#3755 - Deprecate recognizing unicode versions of logical and relational symbols in the parser
Issue -
State: closed - Opened by davidcok over 1 year ago
- 1 comment
Labels: kind: enhancement, part: parser
#3754 - Adding tests for previously uncovered parser code
Pull Request -
State: closed - Opened by davidcok over 1 year ago
#3753 - Bypassing safety checks on universal quantificatoin
Issue -
State: closed - Opened by jtristan over 1 year ago
- 3 comments
Labels: kind: bug, severity: soundness (logic), part: verifier
#3747 - Adding instructions for viewing coverage numbers
Pull Request -
State: closed - Opened by davidcok over 1 year ago
#3743 - Disable gutter icons when verification turned off
Pull Request -
State: closed - Opened by jtristan over 1 year ago
- 1 comment
#3737 - Document: Missing property of map update?
Issue -
State: closed - Opened by davidcok over 1 year ago
- 2 comments
Labels: part: documentation
#3727 - (Test Generation) Fix #3726 bug leading to stack overflow during test generation
Pull Request -
State: open - Opened by Dargones over 1 year ago
#3725 - Incorrect SMT-solver path causes hang
Issue -
State: closed - Opened by RustanLeino over 1 year ago
Labels: kind: bug, part: boogie, part: CLI
#3718 - Add associativity axioms for seq concatentation
Pull Request -
State: open - Opened by atomb over 1 year ago
- 2 comments
#3716 - Allow annotating methods/functions to control inlining for test generation
Issue -
State: closed - Opened by codyroux over 1 year ago
- 6 comments
Labels: kind: enhancement, part: test generation
#3715 - Run integration tests in single process
Pull Request -
State: closed - Opened by keyboardDrummer over 1 year ago
- 2 comments
#3703 - internal error when Keys used as name of a constant
Issue -
State: open - Opened by erniecohen over 1 year ago
Labels: kind: bug, part: verifier, crash, during 2: compilation of correct program
#3660 - Add auditor support for the `:concurrent` attribute
Pull Request -
State: closed - Opened by atomb over 1 year ago
#3645 - Update Boogie to 2.16.3
Pull Request -
State: closed - Opened by atomb over 1 year ago
#3638 - Another attempt at #3622
Pull Request -
State: closed - Opened by atomb over 1 year ago
Labels: run-deep-tests
#3636 - Revert "Update build to use both Z3 4.8.5 and 4.12.1 (#3622)"
Pull Request -
State: closed - Opened by atomb over 1 year ago
Labels: run-deep-tests
#3632 - Imported trait exported as provides should not be usable in extends
Issue -
State: open - Opened by RustanLeino over 1 year ago
Labels: kind: bug, part: resolver, crash, during 1: program development
#3629 - Clean up output of auditor
Pull Request -
State: closed - Opened by atomb over 1 year ago
#3628 - Test improvements discovered as part of Z3 upgrade
Pull Request -
State: closed - Opened by atomb over 1 year ago
#3625 - Add `--verbosity` and `--solver-opt` flags
Pull Request -
State: closed - Opened by atomb over 1 year ago
- 4 comments
#3621 - Crash when calling the main program
Issue -
State: open - Opened by davidcok over 1 year ago
- 1 comment
Labels: kind: bug, part: code-generation, crash, during 2: compilation of correct program
#3613 - Make tests easier in preparation for Z3 4.12.1
Pull Request -
State: closed - Opened by atomb over 1 year ago
#3572 - Crash if cannot find given solver-path
Issue -
State: closed - Opened by davidcok over 1 year ago
Labels: kind: bug
#3568 - Add several new-style command-line options
Pull Request -
State: closed - Opened by atomb over 1 year ago
#3567 - chore(deps): bump pozetroninc/github-action-get-latest-release from 0.5.0 to 0.7.0
Pull Request -
State: open - Opened by dependabot[bot] over 1 year ago
Labels: dependencies, github_actions
#3556 - Detect and report use of mixing options that change semantics
Issue -
State: open - Opened by davidcok over 1 year ago
- 4 comments
Labels: kind: enhancement, logic, crash, priority: not yet, during 3: execution of incorrect program, invalid translated code, introduced: pre-2012
#3555 - Redoing PR3500
Pull Request -
State: closed - Opened by davidcok over 1 year ago
- 1 comment
Labels: run-deep-tests
#3553 - Axiom warnings
Pull Request -
State: closed - Opened by keyboardDrummer over 1 year ago
- 31 comments
#3549 - Dafny crashes with empty command-line argument
Issue -
State: closed - Opened by davidcok over 1 year ago
Labels: kind: bug, severity: crash, part: CLI
#3514 - Devise a single file package for a group of .dfy files (e.g. a library)
Issue -
State: closed - Opened by davidcok over 1 year ago
- 3 comments
Labels: kind: enhancement
#3501 - Investigate Z3 arithmetic mode configuration
Issue -
State: closed - Opened by atomb over 1 year ago
- 1 comment
Labels: kind: enhancement
#3500 - Misc error message improvements and bug fixes: #1637, #3496, #3497, #2200, #2477, #1618, #2830
Pull Request -
State: closed - Opened by davidcok over 1 year ago
#3498 - Adding more quick fixes
Pull Request -
State: closed - Opened by davidcok over 1 year ago
#3494 - Need to fix 2 unstable tests
Issue -
State: closed - Opened by MikaelMayer over 1 year ago
- 1 comment
Labels: kind: language development speed
#3486 - Automated test coverage analysis
Pull Request -
State: closed - Opened by atomb over 1 year ago
- 7 comments
#3468 - Bring new CLI options up to par with legacy options
Issue -
State: open - Opened by atomb over 1 year ago
- 12 comments
Labels: kind: enhancement
#3468 - Bring new CLI options up to par with legacy options
Issue -
State: closed - Opened by atomb over 1 year ago
- 13 comments
Labels: kind: enhancement
#3465 - Dafny to dafny
Pull Request -
State: closed - Opened by jtristan over 1 year ago
#3454 - Add more quick fixes.
Issue -
State: closed - Opened by davidcok over 1 year ago
- 1 comment
Labels: kind: enhancement
#3402 - Bad C# code generation
Issue -
State: open - Opened by ajewellamz over 1 year ago
- 3 comments
Labels: kind: bug, part: code-generation, lang: c#, severity: crash
#3400 - Update tests to work with Z3 4.12.1
Pull Request -
State: closed - Opened by atomb over 1 year ago
- 7 comments
Labels: run-deep-tests
#3385 - Set all Z3 options regardless of Z3 version
Pull Request -
State: closed - Opened by atomb over 1 year ago
#3370 - Array initializers required in contrast to documentation Section 15.1 ?
Issue -
State: closed - Opened by HPGumm over 1 year ago
- 1 comment
Labels: part: documentation
#3361 - /runAllTests exception
Issue -
State: closed - Opened by hmijail over 1 year ago
- 1 comment
Labels: kind: bug
#3360 - Update AutoExtern from the `compiler-bootstrap` branch
Pull Request -
State: closed - Opened by atomb over 1 year ago
- 5 comments
#3358 - "No trigger covering all quantified variables found" is still a warning with `/warningsAsErrors`
Issue -
State: closed - Opened by mattmccutchen-amazon over 1 year ago
Labels: kind: bug, part: resolver
#3346 - Add a missing expression clone
Pull Request -
State: closed - Opened by atomb over 1 year ago
- 1 comment
#3338 - Make a clone of the parsed document available in compilation
Pull Request -
State: closed - Opened by keyboardDrummer over 1 year ago
#3336 - Fix: Modifies clauses with set operations can now be proven
Pull Request -
State: open - Opened by MikaelMayer over 1 year ago
- 1 comment
Labels: need-check-proof-variability
#3329 - Module refinement breaks outline, error reporting and gutter icons
Issue -
State: open - Opened by seebees almost 2 years ago
Labels: kind: bug, part: language server, during 1: program development
#3327 - Intermodular generic trait implementer relationship can lead to malformed Boogie
Issue -
State: open - Opened by fabiomadge over 1 year ago
Labels: kind: bug, part: verifier, crash, during 2: compilation of correct program
#3324 - Fix: Wording of assertion failure closer to semantics
Pull Request -
State: open - Opened by MikaelMayer over 1 year ago
- 1 comment
#3320 - Runtime cast exception in set comprehension
Issue -
State: closed - Opened by mattmccutchen-amazon over 1 year ago
Labels: kind: bug, part: code-generation, lang: golang, lang: js, lang: java, lang: c#, lang: python, priority: next, part: CLI, during 4: bad execution of correct program
#3295 - Convert integration tests to use the new cli
Pull Request -
State: closed - Opened by keyboardDrummer almost 2 years ago
#3268 - crashing with System.OutOfRangeException
Issue -
State: open - Opened by erniecohen almost 2 years ago
Labels: kind: bug, severity: crash
#3262 - crash during type checking
Issue -
State: closed - Opened by davidcok almost 2 years ago
- 1 comment
Labels: kind: bug, crash, priority: next, during 2: compilation of correct program
#3242 - Move installation instructions out of Wiki into dafny.org
Issue -
State: closed - Opened by davidcok almost 2 years ago
- 1 comment
Labels: part: documentation
#3233 - Improve Z3 detection
Pull Request -
State: closed - Opened by atomb almost 2 years ago
#3199 - Simplify fix from PR #3179
Pull Request -
State: closed - Opened by atomb almost 2 years ago
#3181 - Document and improve error messages
Issue -
State: closed - Opened by davidcok almost 2 years ago
- 1 comment
Labels: part: documentation
#3181 - Document and improve error messages
Issue -
State: closed - Opened by davidcok almost 2 years ago
- 1 comment
Labels: part: documentation
#3156 - Bug in verification
Issue -
State: closed - Opened by Ganaham almost 2 years ago
- 2 comments
Labels: kind: bug
#3152 - References to class and iterator type parameters not checked for cardinality preservation
Issue -
State: open - Opened by robin-aws almost 2 years ago
- 4 comments
Labels: kind: bug, priority: not yet, during 3: execution of incorrect program
#3152 - References to class and iterator type parameters not checked for cardinality preservation
Issue -
State: open - Opened by robin-aws almost 2 years ago
- 4 comments
Labels: kind: bug, priority: not yet, during 3: execution of incorrect program
#3150 - Dafny fails to check type characteristics in specification clauses
Issue -
State: closed - Opened by atomb almost 2 years ago
- 4 comments
Labels: kind: bug, part: verifier, priority: next, during 3: execution of incorrect program, introduced: v2.1.0
#3149 - Idea: replace attributes with arbitrary expressions
Issue -
State: open - Opened by robin-aws almost 2 years ago
- 4 comments
Labels: kind: enhancement
#3142 - Cleanups in /testContracts implementation
Pull Request -
State: closed - Opened by atomb almost 2 years ago
#3140 - Name clash and other issues in compiled code for `type` with type variables with the same name
Issue -
State: open - Opened by fabiomadge almost 2 years ago
Labels: kind: bug, part: code-generation, lang: go, lang: java, lang: c#, crash, priority: next, during 1: program development
#3127 - Dafny Python runtime should be published as a PyPI package
Issue -
State: closed - Opened by alex-chew almost 2 years ago
- 2 comments
Labels: kind: enhancement, part: runtime, lang: python
#3109 - Guarantee same diagnostics between `verify` and `server` commands
Issue -
State: open - Opened by keyboardDrummer almost 2 years ago
- 3 comments
Labels: part: language server, kind: language development speed, misc: tests
#3106 - [Feature request]: Use C# Stream instead of manual decoding logic in Scanner.frame
Issue -
State: open - Opened by robin-aws almost 2 years ago
Labels: kind: enhancement, misc: cleanup, part: parser
#3095 - [Feature request]: `{:only}` on assertions
Issue -
State: closed - Opened by MikaelMayer almost 2 years ago
- 13 comments
Labels: kind: enhancement
#3066 - Run the integration tests in a single process to detect usages of static state
Issue -
State: open - Opened by keyboardDrummer almost 2 years ago
- 1 comment
Labels: kind: language development speed