KeY-2.10.0 (2021-12-23)
Core
- IMP: New SMT translation (!312), rework of the SMT communication (!381), and smaller fixes (!394)
- IMP: Renovating the KeY parser (!278)
- IMP: Rewrite of the JML parser in ANTLR (!306) with better exception message (!376)
- IMP: JML-Extension: Assert/Assume and *_free for block contracts (!342)
- FIX: Comment attachment in recoder (!399, !401)
- FIX: Collision of auxiliary contract (!396)
- FIX: Path handling of key files (!395)
- FIX: Pruning in closed branches looses rules (!388, #1480)
- FIX: Repaired file information if a directory is opened in KeY (!386, #1530)
- FIX: Proof loading in the CLI (!385)
- FIX: Invalid URLs under Windows (#1504, !264)
- FIX: lost error messages due to MalformedURLException (!290, #1529)
- FIX: catch headless to make key --auto runnable again (!382)
- FIX:
\singleton
of a non-location (e.g.,\singleton(3)
) now raises an error (!377) - FIX: Completeness gap for array types (!367, #1566)
- FIX: add loop scope unwind (!326)
UI
- IMP: A better dialog for warnings (!374)
- IMP: Performance tuning and fixes for ProofTree (!391)
- IMP: Enables selection of proof in Proof Differences view (!256)
- IMP: Better SourceView Tooltip (!379)
- IMP: Add setting to disable load examples dialog window (!368)
- IMP: Enable syntax highlighting for JML starting with annotation markers (!325)
- FIX: make proof to load from bundle selectable (!237)
- FIX: Escaping comma when saving bookmarked filenames of KeYFileChooser (!387, #1551)
- FIX: make exception dialog able to show files in Jar files (!383)
- FIX: Resolve "SMT Option GUI throws NPE on startup" (!373)
Development
- Enabling of SonarQube in Merge Requests (!323, !378)
- Dependency fixes for Gradle 7 (!372)
We like to thank all the contributor to this release:
Alexander Weigl,
Alicia Appelhagen,
Benjamin Takacs,
Florian Lanzinger,
Jonas Schiffl,
Julian Wiesler,
Lukas Grätz,
Mattias Ulbrich,
Michael Kirsten,
Richard Bubel,
Wolfram Pfeifer