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

#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

#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

#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