What's Changed
- Add Stainless CI workflow for JDK 25 by @vkuncak in #1796
- Pass -XX:+UseCompactObjectHeaders for Java 25 by @vkuncak in #1797
- Download CVC4 from the GitHub archive in stainless-ci.sh by @samarion in #1798
- Fix bigIntToBV literal extraction for unsigned bitvectors by @mbovel in #1799
- Add more end-to-end GenC benchmarks by @mbovel in #1816
- Replace BitVectors with unsigned opaque types UByte, UShort, UInt, ULong by @mbovel in #1817
- Derive documentation version from git tags by @mbovel in #1822
- Reject shifts by exactly the bit width with strict arithmetic by @mbovel in #1815
- GenC: emit immutable values as const by @mbovel in #1809
- Take Int and Long shift amounts modulo the width in verification by @mbovel in #1819
- Publish to a per-run Ivy home in the CI sbt plugin tests by @mbovel in #1829
- Verify the GenC benchmarks with --strict-arithmetic and run them with UBSan by @mbovel in #1825
- Fix GenC on ghost code: unreachable symbols and ghost assignments by @mbovel in #1826
- Move ChooseNothing from false-valid to invalid by @samarion in #1800
- Support empty arrays in GenC by @mbovel in #1832
- CI: cancel superseded pull request runs by @samarion in #1839
- Skip RedBlackTree2 on z3 in VerificationSuite by @samarion in #1840
- Avoid the division in multiplication overflow checks to make them faster by @mbovel in #1830
- Merge the CI workflows into one with a JDK matrix by @mbovel in #1835
- Add an update mode for the expected files of the integration tests by @mbovel in #1837
- Accept field selections as match scrutinees in GenC by @mbovel in #1836
- Make --check-measures=only/no actually filter VCs by @samarion in #1842
- Keep checking VCs in parallel with --debug=stack by @mbovel in #1870
- Drop the scala-parallel-collections dependency by @mbovel in #1868
- Various infrastructure fixes: Docker image, sbt-stainless resolvers, cvc5 licenses by @mbovel in #1856
- Remove JDK 17 CI by @mbovel in #1871
- Keep JVM semantics for max and min on Float and Double by @samarion in #1869
- Accept every registered phase in --debug-phases, wire --admit-all by @mbovel in #1855
- Keep assert messages at extraction and check anonymous class bodies in the fragment checker by @mbovel in #1857
- Run the test suites and their VCs in parallel, fix concurrency bugs by @mbovel in #1867
- Clear pluggedOccMap with the other plugging caches of the lattice simplifier by @mbovel in #1872
- Use Inox's Error tree instead of Stainless's own by @samarion in #1873
- GenC: fix == across classes, zero-filled values, --debug=sizes, and unprintable function types by @mbovel in #1864
- Sort the cases of GenC equality functions by class id by @mbovel in #1875
- Fix the warnings of the CI builds by @mbovel in #1874
- Declare manually defined GenC functions with their code up to the body by @mbovel in #1876
- Cache the solver binaries in CI by @samarion in #1879
- Bump Inox to SMT-LIB semantics and encode the JVM semantics in Stainless by @samarion in #1878
- GenC: fix the initialisation of fixed-length array fields by @mbovel in #1877
- Drop the list of formatted files from .scalafmt.conf by @mbovel in #1880
- GenC: test an array of classes with a single fixed-length array field by @mbovel in #1882
- GenC: replace type aliases with what they stand for by @mbovel in #1884
- GenC: reject returning a class whose subclasses hold an array by @mbovel in #1883
- Raise the VC timeout of FullImperativeSuite to 90 seconds by @mbovel in #1885
- Clean up CI temp folders even when a job fails or is cancelled by @samarion in #1887
- Test that loading a file that does not compile reports the error by @mbovel in #1889
- Add a regression test for a local function with a precondition in a mutable trait by @mbovel in #1890
- Add regression tests for
equalscalls inside case classes by @mbovel in #1888 - Run MsgQueue with codegen and --feeling-lucky again by @mbovel in #1891
- Add a regression test for
ensuringon a body of the wrong type by @mbovel in #1892 - Bump Inox and keep the solvers' strings in the BMP by @samarion in #1886
- Add a regression test for a call dropped by TypeEncoding by @mbovel in #1894
- Add a regression test for a lambda in a counterexample with codegen by @mbovel in #1897
- GenC: emit the last case of a match as the final else by @mbovel in #1881
- Represent Int and Long shifts with trees that take the amount modulo the width by @mbovel in #1858
- Update the expected C of TypeAliases for the final else of matches by @mbovel in #1900
Full Changelog: v0.10.3...v0.10.4