Kani Rust verifier release bundle version 0.25.0.

What's Changed

• Add implementation for the #[kani::should_panic] attribute by @adpaco-aws in #2315
• Upgrade Rust toolchain to nightly-2023-02-04 by @tautschnig in #2324
• Bump CBMC version to 5.80.0 by @zhassan-aws in #2336

Full Changelog: kani-0.24.0...kani-0.25.0

Kani Rust verifier release bundle version 0.24.0.

What's Changed

• Avoid undefined behavior in AnySlice::new() by @feliperodri in #2288
• Create Arbitrary::any_array() by @feliperodri in #2199
• Support symbolic link target directories by @zhassan-aws in #2304
• Update CBMC version to 5.79.0 by @tautschnig in #2301
• Upgrade Rust toolchain to nightly-2023-02-03 by @celinval and @qinheping in #2149 and #2291

Full Changelog: kani-0.23.0...kani-0.24.0

Kani Rust verifier release bundle version 0.23.0.

Breaking Changes

• Remove the second parameter in the kani::any_where function by @zhassan-aws in #2257
  We removed the second parameter in the kani::any_where function (_msg: &'static str) to make the function more ergonomic to use.
  We suggest moving the explanation for why the assumption is introduced into a comment.
  For example, the following code:

    let len: usize = kani::any_where(|x| *x < 5, "Restrict the length to a value less than 5");

should be replaced by:

    // Restrict the length to a value less than 5
    let len: usize = kani::any_where(|x| *x < 5);

Major Changes

• Enable the build cache to avoid recompiling crates that haven't changed, and introduce --force-build option to compile all crates from scratch by @celinval in #2232.
• Add cadical to the list of available solvers by @zhassan-aws in #2217
• Enable loop-contracts synthesis in Kani by @qinheping in #2204
• Improve compilation speed by enabling goto binary serialization by @remi-delmas-3000 in #2205

What's Changed

• Implement Arbitrary for PhantomData and PhantomPinned by @zhassan-aws in #2225
• Fix infinite loop on stub resolution and improve error handling by @celinval in #2227
• Update CBMC version to 5.78 by @remi-delmas-3000 in #2251
• Undo #2194 by @zhassan-aws in #2276

Full Changelog: kani-0.22.0...kani-0.23.0

Kani Rust verifier release bundle version 0.22.0.

Breaking Changes

• The --visualize option now requires --enable-unstable and no longer reports coverage information by @adpaco-aws in #2206

What's Changed

• Allow users to select a subset of harnesses to run by @celinval in #2202
• fix: add kissat to the nixos patchelf list by @camshaft in #2207
• Tone down recommendation and point to bolero by @celinval in #2212
• Bump CBMC version to 5.77.0 by @zhassan-aws in #2216

Full Changelog: kani-0.21.0...kani-0.22.0

Kani Rust verifier release bundle version 0.21.0.

Deprecation Notice

• Ubuntu 18.04 support is deprecated, and will be removed from Kani March 2023.

Major changes

• Allow user to specify CBMC's solver by @zhassan-aws in #2088

What's Changed

• Prevent printing when --quiet is used by @adpaco-aws in #2162
• Gracefully exit from kani-driver process by @celinval in #2168
• Store failure reason into assess metadata by @celinval in #2166
• Bugfix: Handle large bit-widths in traces @adpaco-aws in #2172
• Improve loop handling to avoid spurious loops by @celinval in #2181
• Print reason for failure during assess run by @celinval in #2182
• Fix std overrides in crates where std is used as a feature by @zhassan-aws in #2194
• Bump CBMC version to 5.76.1 by @zhassan-aws in #2183

Full Changelog: kani-0.20.0...kani-0.21.0

What's Changed

• Add support to ubuntu-22.04 by @celinval in #2105
• Add a kani::any_where function to enable easy generation of constrained symbolic values by @danielsn in #2103
• Add --manifest-path and --features by @tedinski in #2085
• Fix postprocessing by also considering unwinding assertion failures from recursion by @adpaco-aws in #2116
• Allow &bool in asserts by @zhassan-aws in #2117
• Remove --legacy-linker support by @celinval in #2127
• Enable concrete playback for satisfiable cover properties by @zhassan-aws in #2134
• Reject proof harnesses with arguments by @celinval in #2132
• Join and format warnings about concurrent constructs by @celinval in #2135
• Add support to casting closure to function pointer by @celinval in #2124
• Account for use statements when resolving paths in kani::stub attributes by @aaronbembenek-aws in #2003
• Include Kissat in the Kani bundle by @zhassan-aws in #2087
• Bump CBMC version by @zhassan-aws in #2067
• Update rust toolchain to 2022-12-11 by @zhassan-aws in #2045
• Bump Dependencies by @rahulku in #2146

Kani Rust verifier release bundle version 0.19.0.

What's Changed

• Introduce cargo kani assess scan for analyzing multiple projects by @tedinski in #2029
• Add support to cdylib, dylib and staticlib by @celinval in #2039
• Allow custom path for installation/setup by @adpaco-aws in #2089
• Fix crash when using public fns reachability by @celinval in #2065
• Implement arbitrary for up to size-12 tuples by @YoshikiTakashima in #2019
• Bump CBMC viewer version to 3.8 by @zhassan-aws in #2043
• Update rustup installation instructions and script by @rahulku in #2095

Full Changelog: kani-0.18.0...kani-0.19.0

Kani Rust verifier release bundle version 0.18.0.

Breaking Changes

• Delete kani::expect_fail function by @zhassan-aws in #2027

What's Changed

• Implement derive macro for Arbitrary by @celinval in #2016
• Introduce a kani macro for checking coverage: kani::cover by @zhassan-aws in #2011
• Publish our crates documentation by @celinval in #1994
• Rename core::assert to avoid possible conflicts in user crate by @zhassan-aws in #2005
• Stop merging all files generated by the compiler by @celinval in #1956
• Resolve paths in kani::stub attributes (ignoring use statements) by @aaronbembenek-aws in #1999
• Report correct package count in assess by @tedinski in #2026
• Amend platform intrinsics documentation by @adpaco-aws in #2030

Full Changelog: kani-0.17.0...kani-0.18.0

Kani Rust verifier release bundle version 0.17.0.

Major Changes

The upgrade to CBMC v5.72.0 greatly improves verification performance for vectors and other data types.

What's Changed

• Validate function/method stubs by @aaronbembenek-aws in #1920
• Fix Arm CBMC architecture name by @tedinski in #1968
• Restore support simd_shl and simd_shr intrinsics by @adpaco-aws in #1964
• Restore support for simd_shuffle* intrinsic by @adpaco-aws in #1961
• Restore support for simd_div and simd_rem intrinsics by @adpaco-aws in #1973
• Use fully qualified paths to avoid harness name clash. by @YoshikiTakashima in #1955
• Fix drop for Struct<dyn T> by @celinval in #1975
• Fix call to core::assert in macro overrides by @zhassan-aws in #1985
• Restrict platform when issuing metadata command by @zhassan-aws in #1987
• Used install toolchain path instead of runtime RUSTUP_HOME by @tedinski in #1988
• Fix drop of Wrapper and fix unsized cast too by @celinval in #1981
• Fix --use-local-bundle argument parsing by @tedinski in #1991
• Bump CBMC to version 5.72.0 by @zhassan-aws in #1941

Full Changelog: kani-0.16.0...kani-0.17.0

Kani Rust verifier release bundle version 0.16.0.

What's Changed

• Allow panic with args to be called in a const context by @zhassan-aws in #1918
• Add support for SIMD vector comparison intrinsics by @adpaco-aws in #1853
• Restore support for bitwise SIMD intrinsics by @adpaco-aws in #1893
• Restore support for some SIMD arithmetic intrinsics by @adpaco-aws in #1931
• Restore simd_extract and simd_insert intrinsics by @adpaco-aws in #1942
• Fix crash for unsupported crate types by @celinval in #1912
• Upgrade rust toolchain to 2022-11-20 by @zhassan-aws in #1927

Full Changelog: kani-0.15.0...kani-0.16.0