kani-0.29.0

Kani Rust verifier release bundle version 0.29.0.

Major Changes

• Create a playback command to make it easier to run Kani generated tests by @celinval in #2464

What Else has Changed

• Fix symtab json file removal and reduce regression scope by @celinval in #2447
• Fix regression on concrete playback inplace by @celinval in #2454
• Fix static variable initialization when they have the same value by @celinval in #2469
• Improve assess and regression time by @celinval in #2478
• Fix playback with build scripts by @celinval in #2477
• Delay printing playback harness until after verification status by @YoshikiTakashima in #2480
• Update rust toolchain to 2023-04-29 by @zhassan-aws in #2452
• Bump CBMC version to 5.84.0 by @tautschnig in #2483

Full Changelog: kani-0.28.0...kani-0.29.0

kani-0.28.0

Kani Rust verifier release bundle version 0.28.0.

Breaking Changes

• The unstable --c-lib option now requires -Z c-ffi to enable C-FFI support by @celinval in #2425

What's Changed

• Enforce unstable APIs can only be used if the related feature is enabled by @celinval in #2386
• Get rid of the legacy mode by @celinval in #2427
• Limit FFI calls by default to explicitly supported ones by @celinval in #2428
• Fix the order of operands for generator structs by @zhassan-aws in #2436
• Add a few options to dump the reachability graph (debug only) by @celinval in #2433
• Perform reachability analysis on a per-harness basis by @celinval in #2439
• Bump CBMC version to 5.83.0 by @zhassan-aws in #2441
• Upgrade the toolchain to nightly-2023-04-16 by @celinval in #2406

Full Changelog: kani-0.27.0...kani-0.28.0

kani-0.27.0

Kani Rust verifier release bundle version 0.27.0.

What's Changed

• Allow excluding packages from verification with --exclude by @adpaco-aws in #2399
• Add size_of annotation to help CBMC's allocator by @tautschnig in #2395
• Implement kani::Arbitrary for Box<T> by @adpaco-aws in #2404
• Use optimized overflow operation everywhere by @celinval in #2405
• Print compilation stats in verbose mode by @celinval in #2420
• Bump CBMC version to 5.82.0 by @adpaco-aws in #2417

Full Changelog: kani-0.26.0...kani-0.27.0

kani-0.26.0

Kani Rust verifier release bundle version 0.26.0.

What's Changed

• Enable Concrete Playback Unit tests to run with --cfg kani by @jaisnan in #2353
• Propogate solver options into synthesizer by @qinheping in #2320
• Docs: Add an "Attributes" section by @adpaco-aws in #2359
• Upgrade Rust toolchain to nightly-2023-02-18 by @tautschnig in #2384
• Bump CBMC version by @karkhaz in #2388

Full Changelog: kani-0.25.0...kani-0.26.0

kani-0.25.0

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-0.24.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-0.23.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-0.22.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-0.21.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

kani-0.20.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