kani-0.36.0

Kani Rust verifier release bundle version 0.36.0.

What's Changed

• Enable -Z stubbing and error out instead of ignoring stub by @celinval in #2678
• Enable concrete playback for failure of UB checks by @zhassan-aws in #2727
• Bump CBMC version to 5.91.0 by @adpaco-aws in #2733
• Rust toolchain upgraded to nightly-2023-09-06 by @celinval @jaisnan @adpaco-aws

Full Changelog: kani-0.35.0...kani-0.36.0

kani-0.35.0

Kani Rust verifier release bundle version 0.35.0.

What's Changed

• Add support to simd_bitmask by @celinval in #2677
• Add integer overflow checking for simd_div and simd_rem by @reisnera in #2645
• Bump CBMC version by @zhassan-aws in #2702
• Upgrade Rust toolchain to 2023-08-19 by @zhassan-aws in #2696

Full Changelog: kani-0.34.0...kani-0.35.0

kani-0.34.0

Kani Rust verifier release bundle version 0.34.0.

Breaking Changes

• Change default solver to CaDiCaL by @celinval in #2557
  By default, Kani will now run CBMC with CaDiCaL, since this solver has outperformed Minisat in most of our benchmarks.
  User's should still be able to select Minisat (or a different solver) either by using #[solver] harness attribute,
  or by passing --solver=<SOLVER> command line option.

What's Changed

• Allow specifying the scheduling strategy in #[kani_proof] for async functions by @fzaiser in #1661
• Support for stubbing out foreign functions by @feliperodri in #2658
• Coverage reporting without a need for cbmc-viewer by @adpaco-aws in #2609
• Add support to array-based SIMD by @celinval in #2633
• Add unchecked/SIMD bitshift checks and disable CBMC flag by @reisnera in #2630
• Fix codegen of constant byte slices to address spurious verification failures by @zhassan in #2663
• Bump CBMC to v5.89.0 by @remi-delmas-3000 in #2662
• Update Rust toolchain to nightly 2023-08-04 by @remi-delmas-3000 in #2661

Full Changelog: kani-0.33.0...kani-0.34.0

kani-0.33.0

Kani Rust verifier release bundle version 0.33.0.

What's Changed

• Adds support for sysconf by @feliperodri in #2557
• Print Kani version by @adpaco-aws in #2619
• Upgrade Rust toolchain to nightly-2023-07-01 by @qinheping in #2616
• Bump CBMC version to 5.88.1 by @zhassan-aws in #2623

Full Changelog: kani-0.32.0...kani-0.33.0

kani-0.32.0

What's Changed

• Add kani::spawn and an executor to the Kani library by @fzaiser in #1659
• Add "kani" configuration key to enable conditional compilation in build scripts by @celinval in #2297
• Adds posix_memalign to the list of supported builtins by @feliperodri in #2601
• Upgrade rust toolchain to nightly-2023-06-20 by @celinval in #2551
• Update rust toolchain to 2023-06-22 by @celinval in #2588
• Automatic toolchain upgrade to nightly-2023-06-24 by @github-actions in #2600
• Bump CBMC version to 5.87.0 by @adpaco-aws in #2598

Full Changelog: kani-0.31.0...kani-0.32.0

kani-0.31.0

Kani Rust verifier release bundle version 0.31.0.

What's Changed

• Add --exact flag by @jaisnan in #2527
• Build the verification libraries using Kani compiler by @celinval in #2534
• Verify all Kani attributes in all crate items upfront by @celinval in #2536
• Throw a graceful error when type checking for ctpop fails by @JustusAdam in #2504
• Bump CBMC version to 5.86.0 by @zhassan-aws in #2561

Full Changelog: kani-0.30.0...kani-0.31.0

kani-0.30.0

Kani Rust verifier release bundle version 0.30.0.

What's Changed

• Remove --harness requirement from stubbing by @celinval in #2495
• Add target selection for cargo kani by @celinval in #2507
• Generate Multiple playback harnesses when multiple crashes exist in a single harness. by @YoshikiTakashima in #2496
• Escape Zero-size types in playback by @YoshikiTakashima in #2508
• Do not crash when rustfmt fails. by @YoshikiTakashima in #2511
• Update Cbmc version by @celinval in #2512
• Upgrade rust toolchain to 2023-04-30 by @zhassan-aws in #2456

Full Changelog: kani-0.29.0...kani-0.30.0

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