dafny-lang/dafny issues and pull requests

#5182 - Document HTML verification coverage reports

Issue - State: open - Opened by atomb 4 months ago
Labels: part: documentation

#5182 - Document HTML verification coverage reports

Issue - State: open - Opened by atomb 4 months ago
Labels: part: documentation

#5181 - Put a message in related location messages, even when using snippets

Pull Request - State: closed - Opened by keyboardDrummer 4 months ago - 2 comments

#5180 - Return a failure exit code when there are warnings and they are not a…

Pull Request - State: open - Opened by keyboardDrummer 4 months ago

#5180 - Return a failure exit code when there are warnings and they are not a…

Pull Request - State: closed - Opened by keyboardDrummer 4 months ago

#5179 - Stop using a cancelled task to present compilation states that could …

Pull Request - State: closed - Opened by keyboardDrummer 4 months ago

#5178 - Do not crash Boogie when an empty {:trigger} attribute occurs

Pull Request - State: closed - Opened by keyboardDrummer 4 months ago

#5178 - Do not crash Boogie when an empty {:trigger} attribute occurs

Pull Request - State: closed - Opened by keyboardDrummer 4 months ago

#5177 - random seed vs verification coverage report?

Issue - State: open - Opened by hmijail 4 months ago - 1 comment
Labels: part: documentation

#5177 - random seed vs verification coverage report?

Issue - State: open - Opened by hmijail 4 months ago - 5 comments
Labels: part: documentation

#5176 - Standard Library documentation is broken

Issue - State: open - Opened by alexporter8013 4 months ago
Labels: part: documentation

#5176 - Standard Library documentation is broken

Issue - State: closed - Opened by alexporter8013 4 months ago
Labels: part: documentation

#5175 - feat: Add newtype support for map and imap

Pull Request - State: closed - Opened by RustanLeino 4 months ago

#5174 - high CPU/RAM usage when should be idle

Issue - State: closed - Opened by hmijail 4 months ago - 24 comments
Labels: kind: bug, area: performance, part: language server, priority: not yet

#5173 - chore(deps): bump softprops/action-gh-release from 1 to 2

Pull Request - State: closed - Opened by dependabot[bot] 4 months ago
Labels: dependencies, github_actions

#5172 - `reveal` should warn instead of error on non-opaque argument

Issue - State: open - Opened by seanmcl 4 months ago
Labels: kind: enhancement, makes-mikael-grateful

#5171 - Peano and single-use integers

Issue - State: open - Opened by GAJaloyan 4 months ago - 6 comments
Labels: kind: enhancement

#5171 - Peano and single-use integers

Issue - State: open - Opened by GAJaloyan 4 months ago - 1 comment
Labels: kind: enhancement

#5170 - fix: Reject modules that were never verified when building doo files

Pull Request - State: open - Opened by robin-aws 4 months ago - 1 comment

#5170 - fix: Reject modules that were never verified when building doo files

Pull Request - State: open - Opened by robin-aws 4 months ago

#5169 - Feature request: Type by class with private memory

Issue - State: open - Opened by MikaelMayer 4 months ago

#5169 - Feature request: Type by class with private memory

Issue - State: open - Opened by MikaelMayer 4 months ago

#5168 - Add syntactic sugar for specifying validity constraints on classes

Issue - State: closed - Opened by keyboardDrummer 4 months ago - 3 comments
Labels: kind: enhancement, part: language definition

#5168 - Add syntactic sugar for specifying validity constraints on classes

Issue - State: closed - Opened by keyboardDrummer 4 months ago - 4 comments
Labels: kind: enhancement, part: language definition

#5167 - Argument-less argument `:trigger` accepted (even encouraged!) but then crashes

Issue - State: open - Opened by RustanLeino 4 months ago
Labels: kind: bug

#5167 - Argument-less argument `:trigger` accepted (even encouraged!) but then crashes

Issue - State: closed - Opened by RustanLeino 4 months ago
Labels: kind: bug, release-blocker

#5166 - Compilation of `:| assume` omitted

Issue - State: open - Opened by RustanLeino 4 months ago - 2 comments
Labels: kind: bug, part: code-generation, priority: next, during 4: bad execution of correct program

#5166 - Compilation of `:| assume` omitted

Issue - State: open - Opened by RustanLeino 4 months ago - 2 comments
Labels: kind: bug, part: code-generation, during 4: execution of correct program

#5165 - Single expression for combined is and as

Issue - State: open - Opened by robin-aws 4 months ago - 5 comments
Labels: kind: enhancement

#5165 - Single expression for combined is and as

Issue - State: open - Opened by robin-aws 4 months ago - 5 comments
Labels: kind: enhancement

#5164 - Remove experimental warning on `--type-system-refresh`

Issue - State: open - Opened by robin-aws 4 months ago
Labels: kind: enhancement, release-blocker

#5164 - Remove experimental warning on `--type-system-refresh`

Issue - State: closed - Opened by robin-aws 4 months ago
Labels: kind: enhancement, release-blocker

#5163 - Remove fragile .expect file that doesn't test much

Pull Request - State: closed - Opened by atomb 4 months ago
Labels: run-deep-tests

#5163 - Remove fragile .expect file that doesn't test much

Pull Request - State: closed - Opened by atomb 4 months ago
Labels: run-deep-tests

#5162 - Use Boogie v3.1.2

Pull Request - State: open - Opened by atomb 4 months ago

#5162 - Use Boogie v3.1.2

Pull Request - State: closed - Opened by atomb 4 months ago

#5161 - Added interface for plugins to add JsonRpcRequestHandlers to the language server

Pull Request - State: open - Opened by BurstingF 4 months ago

#5161 - Added interface for plugins to add JsonRpcRequestHandlers to the language server

Pull Request - State: open - Opened by BurstingF 4 months ago - 1 comment

#5160 - Stuck in verification

Issue - State: open - Opened by MikaelMayer 4 months ago - 5 comments
Labels: kind: enhancement, incompleteness

#5160 - Stuck in verification

Issue - State: open - Opened by MikaelMayer 4 months ago - 7 comments
Labels: kind: enhancement, incompleteness

#5159 - More random seed logging

Pull Request - State: closed - Opened by keyboardDrummer 4 months ago

#5159 - More random seed logging

Pull Request - State: open - Opened by keyboardDrummer 4 months ago

#5158 - Option to run tests for only certain backends

Issue - State: open - Opened by alexporter8013 4 months ago
Labels: kind: enhancement

#5157 - Error message on exception during verification

Pull Request - State: closed - Opened by atomb 4 months ago - 1 comment

#5157 - Error message on exception during verification

Pull Request - State: open - Opened by atomb 4 months ago

#5156 - Crash on running a program on the library backend

Issue - State: open - Opened by robin-aws 4 months ago - 1 comment
Labels: kind: bug, crash

#5156 - Crash on running a program on the library backend

Issue - State: open - Opened by robin-aws 4 months ago - 1 comment
Labels: kind: bug, crash

#5155 - ESDK and DB ESDK nightly builds broken

Issue - State: open - Opened by robin-aws 4 months ago - 1 comment

#5154 - Dafny hangs when verifying certain code

Issue - State: closed - Opened by atomb 4 months ago
Labels: kind: bug, release-blocker

#5154 - Dafny hangs when verifying certain code

Issue - State: open - Opened by atomb 4 months ago
Labels: kind: bug, release-blocker

#5153 - Fix Cycle in type declaration causes crash (#4471)

Pull Request - State: closed - Opened by ssomayyajula 4 months ago

#5153 - Fix Cycle in type declaration causes crash (#4471)

Pull Request - State: open - Opened by ssomayyajula 4 months ago

#5152 - fix: Avoid NPE when building a doo file with —no-verify

Pull Request - State: closed - Opened by robin-aws 4 months ago

#5152 - fix: Avoid NPE when building a doo file with —no-verify

Pull Request - State: closed - Opened by robin-aws 4 months ago

#5151 - Resolution happens x4

Issue - State: open - Opened by MikaelMayer 4 months ago
Labels: kind: bug

#5150 - Add incremental verification progress reporting in a Dafny-centric way

Issue - State: closed - Opened by atomb 4 months ago - 2 comments
Labels: kind: enhancement

#5149 - Fix direction of library implication for --allow-warnings

Pull Request - State: closed - Opened by keyboardDrummer 4 months ago - 1 comment

#5148 - Unable to Prove Object Unchanged After Unrelated Method Call

Issue - State: open - Opened by whonore 4 months ago
Labels: incompleteness

#5147 - Draft: Fix #4127 Too many parens for Python

Pull Request - State: open - Opened by alexporter8013 4 months ago

#5146 - fix: Add uniform checking of type characteristics in refinement modules

Pull Request - State: closed - Opened by RustanLeino 4 months ago

#5145 - StandardLibraries fail to load with `--allow-warnings` flag and throw NPE

Issue - State: closed - Opened by ShubhamChaturvedi7 4 months ago - 2 comments
Labels: kind: bug

#5144 - Type mismatch allowed in ensures clause with type parameters and datatypes

Issue - State: open - Opened by atomb 4 months ago - 4 comments
Labels: kind: bug, during 3: execution of incorrect program

#5143 - Exception when generating doo file with `--no-verify` flag

Issue - State: closed - Opened by ShubhamChaturvedi7 4 months ago - 1 comment
Labels: kind: bug, release-blocker, priority: next

#5142 - Fix: (soundness issue) Twostate predicate now check if their not new arguments are allocated in the previous heap

Pull Request - State: closed - Opened by MikaelMayer 4 months ago

GitHub / dafny-lang/dafny issues and pull requests