Verification framework and tool for higher-order Scala programs
stainless.lang.Cell
and stainless.lang.swap
, allowing to swap the content of two Cells
(#1461)new Array(len)
constructor for primitive types (#1453)ReturnElimination
to avoid triggering AdtSpecialization
(#1466)smt-z3
) to 4.12.2 (#1469)lib
(#1469)stainless-cli
script to invoke scala-cli with the library (#1469)stainless.sh
to stainless
(#1469)--watch
crashing on compilation error (#1424)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.
require
and ensuring
message overloads (#1382)ghost
, assert
and require
arguments by-name (#1364)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.
@opaque
and @inlineOnce
, imperative phase and tupling.This version is tested using java 1.8
static
(#1261)-Dparallel=<N>
when invoking StainlessA VirtualBox image with the release and bolts/ repository clone is available for this version, based on TurnKey linux. Usage:
7zr x stainless-turnkey.7z
obtaining a 2GB .vdi
fileroot
with password neverStainSince2010
cCode.noMangling
annotation and split defines into header and C filesvolatile
and static
keywords to struct fieldscCode.define
functionsscala-3.x
branch only)&&&
operator, which splits verification conditions.require
in inlined functionfull-imperative
phaseopaque
keyword in GenC inlining