Epfl Lara Stainless Versions Save

Verification framework and tool for higher-order Scala programs

v0.9.8.2

6 months ago

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)

v0.9.8.1

7 months ago

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.

v0.9.8

11 months ago

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.

v0.9.7

1 year ago

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

v0.9.6

1 year ago

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)

v0.9.5

2 years ago

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

v0.9.4

2 years ago

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)

v0.9.3

2 years ago

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)

v0.9.2

2 years ago

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)

v0.9.1

2 years ago

Version 0.9.1 (2021-09-28)

Stainless frontend and internals

  • Add the &&& operator, which splits verification conditions.
  • Improve reporting when there are multiple require in inlined function
  • Add some benchmarks for full-imperative phase
  • Upgrade to Scala 2.13 (#1173)

GenC

  • Allow reference to old global state
  • Ignore opaque keyword in GenC inlining