epfl-lara/stainless v0.9.0

Stainless 0.9.0 (2021-08-27)

on GitHub

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, #1113, #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)