epfl-lara/stainless v0.8.1

Stainless 0.8.1 (2021-06-20)

on GitHub

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)
• Improve @traceInduct and add clustering (#1052)
• 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)