Skip to content

Dafny 3.10.0
Compare
Choose a tag to compare
@github-actions github-actions released this 10 Jan 23:54
· 1393 commits to master since this release
v3.10.0
510b679
This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
GPG key ID: 4AEE18F83AFDEB23
Expired
Learn about vigilant mode.

New features

  • Emit warnings about possibly missing parentheses, based on operator precedence and unusual identation (#2783)

  • The DafnyRuntime NuGet package is now compatible with the .NET Standard 2.0 and .NET Framework 4.5.2 frameworks. (#2795)

  • Counterexamples involving sequences present elements in ascending order by index. (#2975)

  • The definition of the char type will change in Dafny version 4, to represent any Unicode scalar value instead of any UTF-16 code unit.
    The new command-line option --unicode-char allows early adoption of this mode.
    See section 7.5 of the Reference Manual for more details.
    (#3016)

  • dafny run now consistently requests UTF-8 output from compiled code.
    Use chcp 65501 if you see garbled output on Windows.
    (#3049)

  • feat: support for traits as type arguments by fully allowing variance on datatypes in Java (#3072)

Bug fixes

  • Function by method with the same name as a method won't crash resolver (#2019)

  • Better reporting if 'this' used in a subset type - and no crash (#2068)

  • Support for aliases in module resolution without crashing on imports (#2108)

  • Added missing check to prevent crash during resolution (#2111)

  • No more resolver crash on pattern match with incompatible types (#2139)

  • Refinements get errors at the correct place in LSP (#2402)

  • Resolution errors in the left-hand sign of an assign-such-that statement do not crash Dafny anymore (#2496)

  • old() cannot be inferred as a trigger alone (#2593)

  • Labels are no longer compiled in the case of variable declarations (#2608)

  • No more mention of reveal lemmas when implementing opaque functions in traits (#2612)

  • Verification of abstract modules not duplicated when imported (#2703)

  • Dafny now compiles functions that mix tail- and non-tail-recursive calls without crashing (#2726)

  • substitution of binding guards does not crash if splits present (#2748)

  • No more crash when constraining type synonyms (#2829)

  • Returning a tuple when it should be two variables does not crash Dafny anymore (#2878)

  • Default generic values no longer cause compilation error (#2885)

  • Now publishing Dafny Binary for MacOS Arm64 architecture (#2889)

  • Added a missing case in the Translator (pattern matching for variable declarations) (#2920)

  • The Python and Go backends now encode non-ASCII characters in string literals correctly (#2926)

  • Added a missing case of TypeSynonymDecl in the resolver that caused a crash (#2927)

  • Fix malformed Boogie generated for extreme predicates (#2984)

  • Counter-examples with non-integer sequence indices do not crash Dafny anymore. (#3048)

  • Use correct type for map update expression (#3059)

  • Language server no longer crashing in special case (#3062)

  • Resolved an instance in which the Dafny language server could enter a broken state. (#3065)

  • Do not refer to an implicit assignment in error messages on return statements (#3125)

  • Multiple exact same failing assertions do not crash the Boogie counter-example engine anymore (#3136)

  • Duplicate declarations caused by resolver do not crash the language server anymore (#3155)

Assets 9
Loading
0 Join discussion