Tags

Version 0.9.7 (2022-11-21)

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

Build

- Include macOS ScalaZ3 build
- Include SBT Stainless plugin

Version 0.9.6 (2022-07-03)

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)

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)

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)

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)

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)
- Example with laws and dynamic dispatch (#1206)

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)
- Example with laws and dynamic dispatch (#1206)

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

Version 0.9.0 (2021-08-27)

Stainless frontend and internals

- Add `--full-imperative` phase, for an imperative phase without aliasing restrictions (#1140)
- Bug fixes in imperative phase (#1108, #1103, #1116, #1121, #1123)
- Split `Unchecked` annotation into `DropVCs` and `DropConjunct` (#1125)
- Fix ghost elimination for multiple parameter groups (#1138)
- Fix timeout sometimes not being respected with non-incremental mode (`no-inc:` solver prefix) (#1141)
- Bump sbt to `1.5.5` and add documentation for Windows (#1134)

GenC

- Drop extern functions in GenC (#1114)
- Disable mangling of fields for classes that are defined outside Stainless (#1115)
- Add pure attribute to pure functions when compiling to C (#1119)
- Split `inline` (for verification) and `cCode.inline` (for compilation) annotations (#1132)
- Reorganize GenC annotations (#1129)
- Bug fixes (#1124, #1133)

Stainless Noxt 0.8.1-1-g3c34688 (2021-07-21)

Stainless Noxt 0.8.1 (2021-06-23)

Release Notes

Version 0.8.1 (2021-06-20)

Stainless frontend and internals

- Better support for jumping to errors in IDEs (#966, #995, #996)
- Add support for return keyword (#923, #925, #934)
- Various fixes and changes in aliasing analysis (#915, #918, #920, #928, #965, #969, #973, #985, #1076, #1094)
- Support for tuples with mutable types (#1064)
- Add support for multiple requires in functions (not in ADTs) (#983)
- Better measure inference for chain processor (#967)
- Add more support for bitvector operations (#962, #1062)
- Print verification progress but not all verification conditions by default (#1018)
- Add support for swap operation for array elements (#946)
- Add support for inlining and making opaque while loops (#1009)
- Library cleanup (#953, #998, #999, #1000)
- Add fresh copy primitive (#1033)
- Add no-return invariants for while loops (#1079)

SMT solvers

- Add support for CVC4 1.8 (#833)
- Add support for Z3 4.8.10 (#1010)

GenC

- Better support for ``@export`` annotation in GenC (#924, #1008, #1019)
- Add StructInliningPhase to remove structs with one member in GenC (#1058, #1065)
- Add support for fixed length arrays in GenC (#1055, #1057)
- Add compilation of global state in GenC (#1085, #1089)

Stainless Noxt v0.8.0

Version 0.8.0 (2021-02-24)

Features

- Support for Scala 2.12.13 (#913)
- Support for ghost fields in GenC (#904, #907)
- Initial support for unsigned integers in GenC (#888)

Bug fixes

- Fix issues watch mode (and add support for Enter key to reload) (#906)
- Better support for refinement types in type-checker
- Various bug fixes in extraction phases

After this commit, the counter encoding of allocation was dropped

Version 0.7.6 (2021-01-18)

Features

- Add GenC component from Leon (#885)
- Add frontend for more bitvector types and operations (#879)

Improvements

- Inox dependency is now directly on GitHub

Bug fixes

- Fix some issues in imperative phase (#874) and type encoding (#884)

Version 0.7.5 (2020-11-27)

Features

- Add `admit-vcs` option to generate VCs without sending them to the solver
- Add support for indexed types in scalac frontend

Improvements

- Generalize specification helpers (#828)

Bug fixes

- Remove unsound type-checking rule for function types, and add subtying rules instead

Version 0.7.4 (2020-10-02)

Bug fixes

- Fix unapplyAccessor not instantiating with refinement type (#841)
- Remove duplicate serializations

Version 0.7.3 (2020-09-08)

Improvements

- Remove check that measure has good type at call site (this was making arguments of recursive functions being type-checked twice, and thus duplicating VCs)
- Instead, add check that mutually recursive functions have the same measure type
- `SplitCallBack` now processes mutually recursive functions together
- Improve HTML output for type-checking derivation

Version 0.7.2 (29-08-2020)

Features

- Add `ListMap` implementation (associative list) (#794)

Improvements

- Remove type-checking tuple rule that was duplicating VCs (#792)
- Improve documentation on check/assert (#815)
- Add documentation for contracts on abstract functions (#825)

Bug fixes

- Fix `@induct` transformation for bounded-size integers (#804)
- Add checks to reject programs not supported by Stainless (#810, #814)
- Fix type encoding translation error (#818)
- Fix issues on `@inlineInvariant` feature (#820)
- Fix bug where Stainless could make an infinite loop in `isMutableClassType` (#824)
- Fix "missing field" error in watch mode (#829)
- Fix bug in watch mode where errors from previous runs kept getting reported (#830)
- Fix bug in watch mode that made the verification report incomplete (#831)