v0.9.8.7: Version 0.9.8.7 (2024-05-06)

Version 0.9.8.7 (2024-05-06)

Stainless frontend, library and internals

• Add stainless.lang.Try allowing for a monadic try construct (#1515)
• Upgrade the Scala 3 frontend to Scala 3.3.3 (#1514 and #1516)
• Avoid rebuilding mutated objects when possible in AntiAliasing (#1507 and #1509)
• Show the ID of the corresponding generated SMT-lib file for each VC in the summary when debug=smt option is enabled (#1508)
• Have isExpressionFresh consider arguments when computing freshness of a function call (#1505)
• Avoid pairwise matching of "external" methods in Equivalence checking mode (#1503)
• Fix in documentation (#1502)
• Add support for exported methods (#1501)
• Fix ImperativeCleanup phase to not clean some unused bindings that should not be removed (#1500)
• Fix a bug in Equivalence checking mode that was considering the wrong preconditions in some cases (#1499)
• Fix type alias of opaque triggering missing dependencies (#1498)
• Add missing dropVCs annotation in AntiAliasing (#1496)
• Relax fallback condition of AntiAliasing handling of Let (#1495)
• Add missing case for Array typeBounds, make private final, fix minor bug in RefinementLifting (#1494)
• Fix MatchError in EffectsAnalyzer leading to a crash in some cases (#1492)
• Fix parametric extension methods (#1490)
• Allow for redundant type checks for pattern matching (#1489)
• Add 'unknown safety' category for Equivalence checkign (#1488)
• Allows for let-binding in tests and output 'expected but got' results in Equivalence checking (#1485)
• Add a tail recursive implementation of map for mutable tail lists as a benchmark (#1484)

Build

• Fix the stainless-cli script (#1486)

Stainless 0.9.8.2 (2023-11-10)

Version 0.9.8.2 (2023-11-10)

Stainless frontend, library and internals

• Add stainless.lang.Cell and stainless.lang.swap, allowing to swap the content of two Cells (#1461)
• Add support for cvc5 (#1444)
• Upgrade the Scala 3 frontend to Scala 3.3 (#1442)
• Upgrade the Scala 2 frontend to Scala 2.13.12 (#1469)
• Support for new Array(len) constructor for primitive types (#1453)
• Remove ensuring clause in ghost elimination (#1454)
• Fix while loops being mistakenly considered as ghost (#1467)
• Fix occasionally incorrect positions (#1447, #1455, #1473, #1477)
• Enforce purity for class invariants (#1475)
• Do not treat inline methods or functions as ghost (#1481)
• Applying some type widening in ReturnElimination to avoid triggering AdtSpecialization (#1466)
• Relax freshness condition and improve aliasing error messages (#1468)

Build

• Upgrade the shipped Z3 version (smt-z3) to 4.12.2 (#1469)
• Add cvc5 1.0.8 to the archive (#1469)
• Add arm64 build for macOS (#1469)
• Add the compiled and source code of the Stainless library to the archive, under lib (#1469)
• Add a stainless-cli script to invoke scala-cli with the library (#1469)
• Rename stainless.sh to stainless (#1469)

Stainless 0.9.8.1 (2023-09-21)

Version 0.9.8.1 (2023-09-21)

Stainless frontend, library and internals

• Fix --watch crashing on compilation error (#1424)
• Expand options for equivalence checking (#1422, #1435)
• Add more info messages (#1425)
• Add further postconditions for indexOf and apply (#1428)
• Documentation updates (#1429, #1434, #1431)
• Fix ghost elimination for GenC (#1433)
• Reorganize some library files and allow for verification without Stainless library (#1436)
• Fix issue #1399

Note on platforms

Our CI and most developer machines run Ubuntu 20 or 22; we use OpenJDK 17. Stainless runs fine on terminal-only Linux installations (without X or Wayland), which makes it easy to deploy in Window Subsystem for Linux on Windows; we recommend WSL with *-linux.zip release file for Windows as well (though *-win.zip should work as well). Use option --solvers=smt-z3 on Mac.

Stainless 0.9.8 (2023-05-30)

Version 0.9.8 (2023-05-30)

Stainless frontend, library and internals

• Expand Stainless library (#1400, #1402, #1418)
• Improved reporting (#1396, #1410)
• Support for enum case objects (#1384)
• Support require and ensuring message overloads (#1382)
• Make ghost, assert and require arguments by-name (#1364)
• Move equivalence checking to a component (#1378)
• Some improvements to OL and OCBSL based simplifiers (#1380)
• Fix issues #1343, #1214, #1351, #1352, #1353, #1365, #1379, #1389, #1390, #1377, #1349, #1405, #1401

Note on platforms

Our CI and most developer machines run Ubuntu 20 or 22; we use OpenJDK 17. Stainless runs fine on terminal-only Linux installations (without X or Wayland), which makes it easy to deploy in Window Subsystem for Linux on Windows; we recommend WSL with *-linux.zip release file for Windows as well (though *-win.zip should work as well). Use option --solvers=smt-z3 on Mac.

Stainless 0.9.7 (2022-11-21)

Version 0.9.7 (2022-11-21)

General

• The recommended JDK is now JDK 17

Stainless frontend, library and internals

• Improve equivalence checking: function call matching, norm, mkTest (#1294)
• Experimental integration of OL- and OCBSL- based simplifiers (#1315)
• Upgrade to Scala 3.2 (#1317)
• Add verification pipeline summary (#1336)
• Fix issues #1332, #1271, #1333, #731, #1290, #1321, #1322, #1306, #1301, #1302, essentially concerning @opaque and @inlineOnce, imperative phase and tupling.

Build

• Include macOS ScalaZ3 build
• Include SBT Stainless plugin

Stainless 0.9.6 (2022-07-03)

Version 0.9.6 (2022-07-03)

This version is tested using java 1.8

Stainless frontend, library and internals

• Fix issues #1268 #1269 #1270 #1272 #1273 #1274 (#1277)
• Avoid unnecessary capture of PC variables when hoisting functions (#1265)
• Minor fixes (#1260, #1263, #1280, #1292)

GenC

• Annotate unexported function as static (#1261)

Stainless 0.9.5 (2022-05-06)

Version 0.9.5 (2022-05-06)

Stainless frontend, library and internals

• VC checking in parallel (#1247)
  • The parallelism can be specified with -Dparallel=<N> when invoking Stainless
• Fix issue #1159 (#1246)
• Address some issues in the imperative phase (#1245, #1252)

VirtualBox VDI Image

A VirtualBox image with the release and bolts/ repository clone is available for this version, based on TurnKey linux. Usage:

• download (648MB)
• extract the archive using 7zr x stainless-turnkey.7z obtaining a 2GB .vdi file
• set up a VM machine as Linux with enough memory and cores and the previously extracted VDI image as the disk
• boot the machine in VirtualBox
• Quit the console dialog that pops at boot
• log in as root with password neverStainSince2010
• Invoke the script in the home directory for a test run and browse for more examples

Stainless 0.9.4 (2022-03-11)

Version 0.9.4 (2022-03-11)

Stainless frontend, library and internals

• Pass the -Ysafe-init option to Dotty (#1242)
• Experimental test cases generation (#1239)
• Fix issue #1051 (#1219)
• PC for local classes capturing variables (#1210)

Build

• Do not duplicate ScalaZ3 jars (#1241)

Stainless 0.9.3 (2022-02-25)

Version 0.9.3 (2022-02-25)

GenC

• Add cCode.noMangling annotation and split defines into header and C files
• Propagate volatile and static keywords to struct fields
• Avoid trimming of cCode.define functions
• Introduce a binding to 'guard' against references created by the Referentiator (#1235)

Build

• Windows build (#1234)

Stainless 0.9.2 (2022-01-17)

Version 0.9.2 (2022-01-17)

Stainless frontend, library and internals

• Main list operations with Int instead of BigInt indices (#1225)
• Scala 3 extraction frontend (#1216, scala-3.x branch only)
• Adapt Coq build to 8.14.0 (#1198)
• Improve handling of Enter key in watch mode (#1195)
• Fix extraction of f => g style renamed imports (#1193)
• Add sizes debug option to display size statistics after each phase (#1185)
• Remove simplifications in VC building to avoid big slowdown (#1184)

GenC

• Split header and C includes (#1204)
• Better header extraction in GenC cCode.function annotation (#1203)
• Extract header from manually defined definition in Genc (#1200)
• Add missing assert cases in GenC deconstructors (#1199)
• Bump sbt-assembly version, more parentheses and relax arrays checks in GenC (#1197)
• Add support for initializing complex expressions with memset 0 (#1196)
• Fix GenC duplicate reporting and add cCode.define annotation (#1192)
• Fix some GenC export issues and add cCode.pack annotation (#1190)
• Remove parentheses from dropped constants in GenC (#1189)
• cCode.drop shouldn't always imply extern (#1188)
• Use primitive equality for TypeDefType in GenC (#1187)
• Fix typo in sizes debug output (#1186)

Documentation

• Add documentation for some annotations and keywords (#1183)
• Doc fixes (#1220)