dafny-lang/dafny issues and pull requests

#1760 - Verifications with an `assume`

Issue - State: open - Opened by seebees over 2 years ago - 3 comments
Labels: misc: question, priority: not yet

#1732 - `DafnyAST` and `Resolver` shouldn't depend on the choice of compiler target

Issue - State: open - Opened by cpitclaudel over 2 years ago
Labels: part: code-generation, misc: cleanup, kind: language development speed

#1731 - Incorrect `type test for … must be from an expression assignable to it` message, resolved by adding a type annotation

Issue - State: open - Opened by cpitclaudel over 2 years ago - 4 comments
Labels: kind: bug, part: resolver, area: error-reporting

#1678 - IDE shows "Verified", but input contains a resolution error

Issue - State: open - Opened by cpitclaudel over 2 years ago
Labels: kind: bug, part: language server, difficulty: good-first-issue, during 1: program development

#1658 - Add opinionated auto-formatter for Dafny source code

Issue - State: closed - Opened by alex-chew almost 3 years ago - 2 comments
Labels: kind: enhancement, priority: next

#1658 - Add opinionated auto-formatter for Dafny source code

Issue - State: closed - Opened by alex-chew almost 3 years ago - 2 comments
Labels: kind: enhancement, priority: next

#1636 - CI build sometimes fails because coco crashes

Issue - State: closed - Opened by keyboardDrummer almost 3 years ago - 1 comment
Labels: part: parser

#1588 - Termination of dynamic dispatch

Issue - State: open - Opened by RustanLeino almost 3 years ago - 14 comments
Labels: kind: enhancement, part: verifier

#1570 - Assert failing in strange way

Issue - State: open - Opened by hmijail almost 3 years ago - 10 comments
Labels: kind: enhancement, part: verifier, misc: instability

#1566 - Update VS Code plugin gif

Issue - State: open - Opened by robin-aws almost 3 years ago - 7 comments
Labels: kind: bug, misc: cleanup

#1565 - `DafnyPipeline.Test` build error

Issue - State: open - Opened by hirataqdees almost 3 years ago - 3 comments
Labels: kind: bug, misc: cleanup, kind: language development speed

#1554 - Lit updates

Pull Request - State: closed - Opened by RustanLeino almost 3 years ago - 2 comments

#1542 - lambda expression passed to extreme lemma causes crash

Issue - State: open - Opened by RustanLeino almost 3 years ago
Labels: kind: bug, part: verifier, severity: crash

#1541 - Type-test binding not compiled correctly

Issue - State: open - Opened by RustanLeino almost 3 years ago
Labels: kind: bug, part: code-generation, lang: go, lang: js, lang: java, lang: c#, lang: c++, priority: next, during 4: execution of correct program

#1533 - Unary minus on bitvector type synonym causes crash

Issue - State: open - Opened by RustanLeino almost 3 years ago - 1 comment
Labels: part: verifier, difficulty: good-first-issue, severity: crash

#1530 - Move runtimes into distinct project in the solution

Issue - State: open - Opened by camrein almost 3 years ago - 5 comments
Labels: kind: language development speed

#1500 - Smoke tests report unreachable code because of bpl

Issue - State: open - Opened by xtrm0 almost 3 years ago - 3 comments
Labels: kind: bug, misc: update

#1493 - Ignored test: ChangeDocumentRightAfterOpeningCancelsLoad

Issue - State: open - Opened by robin-aws almost 3 years ago
Labels: misc: cleanup, kind: language development speed

#1481 - Resolution crash when refining a module and defining a const with a subset type

Issue - State: open - Opened by robin-aws almost 3 years ago
Labels: kind: bug, part: resolver, area: refinement, severity: crash

#1441 - Feature request: explicit language features for verification debugging

Issue - State: open - Opened by robin-aws about 3 years ago - 3 comments
Labels: kind: enhancement, priority: not yet

#1427 - datatype doesn't correctly compute equality-support

Issue - State: open - Opened by tjhance about 3 years ago - 3 comments
Labels: kind: bug, part: resolver, priority: not yet, during 3: execution of incorrect program, introduced: pre-2012

#1390 - Contract.Assert does not cause failures in published Dafny builds

Issue - State: open - Opened by robin-aws about 3 years ago - 5 comments
Labels: misc: cleanup, kind: language development speed, crash

#1373 - Verification: map should not allow .Values if the value type is not equality supporting

Issue - State: closed - Opened by sorawee about 3 years ago - 3 comments
Labels: kind: bug, severity: soundness (logic), part: resolver

#1367 - Go: bug in multiple occurrences of the same key in map

Issue - State: closed - Opened by sorawee about 3 years ago - 8 comments
Labels: kind: bug, lang: go, lang: js, part: verifier, severity: soundness (wrong result)

#1352 - `Expect` not allowed in function methods?

Issue - State: closed - Opened by hmijail about 3 years ago - 8 comments
Labels: kind: enhancement

#1344 - rise4fun can't open now,is there any backup link?

Issue - State: open - Opened by Aaron-clou about 3 years ago - 1 comment
Labels: kind: enhancement, misc: cleanup

#1329 - "Dependabot can't parse your Gemfile.lock"

Issue - State: open - Opened by robin-aws about 3 years ago
Labels: misc: cleanup, kind: language development speed

#1316 - Exception in `Translator.GetField`

Issue - State: open - Opened by keyboardDrummer about 3 years ago
Labels: kind: bug, part: verifier, severity: crash

#1314 - Several tests don't pass on Windows

Issue - State: open - Opened by keyboardDrummer about 3 years ago
Labels: misc: cleanup, platform: windows, kind: language development speed

#1291 - Output issue in compile:3 for Java

Issue - State: open - Opened by sorawee about 3 years ago - 4 comments
Labels: kind: bug, lang: java, misc: cleanup

#1259 - C++ support for unconstrained ints

Issue - State: open - Opened by robin-aws over 3 years ago - 6 comments
Labels: kind: enhancement, part: code-generation, misc: update, lang: c++

#1226 - Non-reference traits

Issue - State: closed - Opened by RustanLeino over 3 years ago - 3 comments
Labels: kind: enhancement, part: language definition

#1170 - Duplicate :extern name causes crash

Issue - State: open - Opened by RustanLeino over 3 years ago
Labels: kind: bug, part: verifier, severity: crash

#1153 - Documentation: hard to figure out how to run Boogie manually

Issue - State: open - Opened by tchajed over 3 years ago - 8 comments
Labels: part: documentation

#1120 - Some function allocatedness test are suppressed

Issue - State: open - Opened by RustanLeino over 3 years ago - 1 comment
Labels: kind: bug, part: verifier, priority: not yet, during 3: execution of incorrect program, introduced: 2.0.0

#1104 - Using Java keyword as filename causes crash

Issue - State: open - Opened by RustanLeino over 3 years ago
Labels: kind: bug, part: code-generation, lang: java, severity: crash

#1026 - Add behavior of collection axioms

Issue - State: open - Opened by davidcok over 3 years ago
Labels: part: verifier, status: implemented, misc: cleanup, kind: language development speed

#995 - Resolution of names in dependency analysis

Issue - State: open - Opened by davidcok almost 4 years ago
Labels: misc: cleanup, kind: language development speed

#960 - Doc: Outstanding formatting issues for the reference manual

Issue - State: open - Opened by davidcok almost 4 years ago - 1 comment
Labels: part: documentation

#738 - License copyright

Issue - State: open - Opened by davidcok about 4 years ago
Labels: kind: bug, misc: cleanup

#620 - Issue a warning on pre-conditions (requires) equivalent to false

Issue - State: closed - Opened by franck44 over 4 years ago - 1 comment
Labels: kind: enhancement

#601 - Emit Rust code

Issue - State: closed - Opened by johnterickson over 4 years ago - 4 comments
Labels: kind: enhancement, priority: not yet

#540 - Malformed Java target code for unreachable code

Issue - State: open - Opened by RustanLeino over 4 years ago - 2 comments
Labels: part: code-generation, lang: java, severity: crash

#511 - Parser should not dynamically inject shared builtin program components

Issue - State: closed - Opened by robin-aws over 4 years ago - 6 comments
Labels: kind: enhancement, part: runtime, part: parser, area: build-system

#494 - Dafny Go runtime (Binaries/DafnyRuntime.go) should be published as a Go module

Issue - State: open - Opened by robin-aws over 4 years ago - 5 comments
Labels: kind: enhancement, lang: golang, part: runtime

#266 - /compile:3 C# compiler doesn't find library DLL and crashes

Issue - State: open - Opened by mschlaipfer over 5 years ago - 2 comments
Labels: kind: bug, part: code-generation, area: ffi, severity: crash

GitHub / dafny-lang/dafny issues and pull requests