Skip to content
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)