dafny-lang/dafny issues and pull requests

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

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

#1421 - Lemmas not working properly inside of old()

Issue - State: closed - Opened by erniecohen almost 4 years ago - 1 comment
Labels: kind: bug, part: verifier, priority: not yet, status: fixed

#1414 - Java: compilation error on nested array

Issue - State: closed - Opened by sorawee about 4 years ago - 4 comments
Labels: kind: bug, part: code-generation, lang: java, priority: not yet, status: fixed

#1411 - NullReferenceException in Compiler

Issue - State: closed - Opened by IsaacOscar about 4 years ago - 1 comment
Labels: kind: bug, part: code-generation, crash, priority: not yet, status: fixed

#1402 - Problem with set of arrays

Issue - State: closed - Opened by sorawee about 4 years ago - 1 comment
Labels: kind: bug, part: code-generation, lang: js, lang: java, priority: not yet, status: fixed

#1401 - internal translation error for type parameter

Issue - State: closed - Opened by IsaacOscar about 4 years ago - 1 comment
Labels: kind: bug, part: verifier, priority: not yet, status: fixed

#1397 - Java 8: compilation error from tuple + if expression

Issue - State: closed - Opened by sorawee about 4 years ago - 2 comments
Labels: kind: bug, part: code-generation, lang: java, priority: not yet, status: fixed

#1396 - C#: compilation error on if expression of arrow type

Issue - State: closed - Opened by sorawee about 4 years ago - 1 comment
Labels: kind: bug, part: resolver, priority: not yet, status: fixed

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

Issue - State: open - Opened by robin-aws about 4 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 4 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 4 years ago - 8 comments
Labels: kind: bug, lang: go, lang: js, part: verifier, severity: soundness (wrong result)

#1365 - C#: compilation error for sequence comprehension

Issue - State: closed - Opened by sorawee about 4 years ago - 1 comment
Labels: kind: bug, lang: c#, priority: not yet, status: fixed

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

Issue - State: closed - Opened by hmijail about 4 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 4 years ago - 1 comment
Labels: kind: enhancement, misc: cleanup

#1331 - Assumption failed from too deeply nested AST, resulting in a hard crash

Issue - State: closed - Opened by sorawee about 4 years ago - 3 comments
Labels: kind: bug, part: resolver, crash, priority: not yet, status: fixed

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

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

#1316 - Exception in `Translator.GetField`

Issue - State: closed - Opened by keyboardDrummer about 4 years ago - 1 comment
Labels: kind: bug, part: verifier, crash, priority: not yet, status: fixed

#1314 - Several tests don't pass on Windows

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

#1297 - Dafny generates invalid Java code

Issue - State: closed - Opened by sorawee about 4 years ago - 1 comment
Labels: kind: bug, lang: java, priority: not yet, status: fixed

#1291 - Output issue in compile:3 for Java

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

#1259 - C++ support for unconstrained ints

Issue - State: open - Opened by robin-aws about 4 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 4 years ago - 3 comments
Labels: kind: enhancement, part: language definition

#1209 - Dafny can't have a static constant called `IsLimit` or `IsNat`, and a few others

Issue - State: closed - Opened by seanmcl over 4 years ago - 4 comments
Labels: kind: bug, part: documentation, part: resolver, priority: not yet, status: fixed

#1170 - Duplicate :extern name causes crash

Issue - State: closed - Opened by RustanLeino over 4 years ago - 1 comment
Labels: kind: bug, part: verifier, crash, priority: not yet, status: fixed

#1162 - incompleteness in sequence extensionality proofs (possibly caused by boxing)

Issue - State: closed - Opened by tjhance over 4 years ago - 4 comments
Labels: kind: bug, part: verifier, incompleteness, priority: not yet, status: fixed

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

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

#1120 - Some function allocatedness test are suppressed

Issue - State: open - Opened by RustanLeino over 4 years ago - 3 comments
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: closed - Opened by RustanLeino over 4 years ago - 1 comment
Labels: kind: bug, part: code-generation, lang: java, crash, priority: not yet, status: fixed

#1097 - regression in literal function unfolding proofs

Issue - State: closed - Opened by tjhance over 4 years ago - 5 comments
Labels: kind: bug, part: verifier, priority: not yet, status: fixed

#1026 - Add behavior of collection axioms

Issue - State: open - Opened by davidcok over 4 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 over 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 over 4 years ago - 1 comment
Labels: part: documentation

#860 - confusion of same member type name from different modules

Issue - State: closed - Opened by erniecohen almost 5 years ago - 2 comments
Labels: kind: bug, part: verifier, priority: not yet, status: fixed

#858 - Errors from malformed Boogie should be marked as internal error

Issue - State: closed - Opened by RustanLeino almost 5 years ago - 3 comments
Labels: kind: bug, part: verifier, priority: not yet, status: fixed

#738 - License copyright

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

#670 - Incorrect fuel parameter used in method override check

Issue - State: closed - Opened by RustanLeino about 5 years ago - 1 comment
Labels: kind: bug, part: verifier, priority: not yet, status: fixed

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

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

#617 - Opaque type marked "extern" should not prevent compilation

Issue - State: closed - Opened by danmatichuk over 5 years ago - 2 comments
Labels: kind: bug, part: code-generation, area: ffi, priority: not yet, status: fixed

#601 - Emit Rust code

Issue - State: open - Opened by johnterickson over 5 years ago - 3 comments
Labels: kind: enhancement

#540 - Malformed Java target code for unreachable code

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

#531 - C# compiler error when generated lambda refers to out parameter

Issue - State: closed - Opened by lukemaurer over 5 years ago - 1 comment
Labels: kind: bug, part: code-generation, lang: c#, priority: not yet, status: fixed

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

Issue - State: closed - Opened by robin-aws over 5 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 5 years ago - 5 comments
Labels: kind: enhancement, lang: golang, part: runtime

#422 - Opaque functions cause failing override checks

Issue - State: closed - Opened by RustanLeino almost 6 years ago - 1 comment
Labels: kind: bug, part: verifier, priority: not yet, status: fixed

#359 - Predicates containing higher-order assertions behave oddly

Issue - State: closed - Opened by csgordon about 6 years ago - 9 comments
Labels: kind: bug, part: verifier, priority: not yet, status: fixed

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

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

#259 - issue in datatype/module name conflict

Issue - State: closed - Opened by gancherj about 6 years ago - 1 comment
Labels: kind: bug, part: code-generation, area: ffi, priority: not yet

#255 - dafny fails to deduce body of function across an abstract module boundary

Issue - State: closed - Opened by tjhance over 6 years ago - 3 comments
Labels: kind: bug, part: resolver, area: refinement, part: verifier, incompleteness, has-workaround: yes, status: needs-decision, priority: not yet, status: fixed

#146 - Allow forall statements in expressions

Issue - State: closed - Opened by wilcoxjay almost 8 years ago - 3 comments
Labels: kind: enhancement, part: verifier, part: parser, status: designed, difficulty: easy, priority: not yet

GitHub / dafny-lang/dafny issues and pull requests