You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
This commit was created on GitHub.com and signed with GitHub’s verified signature.
The key has expired.
feat: continue statements. Like Dafny's break statements, these come in two forms: one that uses a label to name the continue target and one that specifies the continue target by nesting level. See section 19.2 of the Reference Manual. (#1839)
feat: The keyword syntax for functions will change in Dafny version 4. The new command-line option /functionSyntax (see /help) allows early adoption of the new syntax. (#1832)
feat: Attribute {:print} declares that a method may have print effects. Print effects are enforced only with /trackPrintEffects:1.
feat: Add support for non-interactive solvers that need all SMT-Lib input in one batch (enabled with /proverOpt:BATCH_MODE=true). Inherited from Boogie 2.13 (boogie-org/boogie#512).
fix: Allow /verificationLogger and /vcsCores to be usable together. Inherited from Boogie 2.13 (boogie-org/boogie#515).
fix: Plug two memory leaks in Dafny's verification server. (#1858, #1863)
fix: No warning "File contains no code" if a file only contains a submodule (#1840)
fix: Stuck in verifying in VSCode - support for verification cancellation (#1771)
fix: export-reveals of function-by-method now allows the function body to be ghost (#1855)
fix: Regain C# 7.3 compatibility of the compiled code. (#1877)
fix: The error "assertion violation" is replaced by the better wording "assertion might not hold". This indicates better that the verifier is unable to prove the assertion. (#1862)