This file contains notable changes (e.g. breaking changes, major changes, etc.) in Kani releases.
This file was introduced starting Kani 0.23.0, so it only contains changes from version 0.23.0 onwards.
- Do not assume that ZST-typed symbols refer to unique objects by @tautschnig in model-checking#3134
- Remove
kani::Arbitrary
from themodifies
contract instrumentation by @feliperodri in model-checking#3169 - Emit source locations whenever possible to ease debugging and coverage reporting by @tautschnig in model-checking#3173
- Rust toolchain upgraded to
nightly-2024-04-21
by @celinval
Full Changelog: https://github.com/model-checking/kani/compare/kani-0.50.0...kani-0.51.0
- Fix compilation issue with proc_macro2 (v1.0.80+) and Kani v0.49.0 (model-checking#3138).
- Implement valid value check for
write_bytes
by @celinval in model-checking#3108 - Rust toolchain upgraded to 2024-04-15 by @tautschnig @celinval
Full Changelog: https://github.com/model-checking/kani/compare/kani-0.49.0...kani-0.50.0
- Disable removal of storage markers by @zhassan-aws in model-checking#3083
- Ensure storage markers are kept in std code by @zhassan-aws in model-checking#3080
- Implement validity checks by @celinval in model-checking#3085
- Allow modifies clause for verification only by @feliperodri in model-checking#3098
- Add optional scatterplot to benchcomp output by @tautschnig in model-checking#3077
- Expand ${var} in benchcomp variant
env
by @karkhaz in model-checking#3090 - Add
benchcomp filter
command by @karkhaz in model-checking#3105 - Upgrade Rust toolchain to 2024-03-29 by @zhassan-aws @celinval @adpaco-aws @feliperodri
Full Changelog: https://github.com/model-checking/kani/compare/kani-0.48.0...kani-0.49.0
- We fixed a soundness bug that in some cases may cause Kani to not detect a use-after-free issue in model-checking#3063
- Fix
codegen_atomic_binop
foratomic_ptr
by @qinheping in model-checking#3047 - Retrieve info for recursion tracker reliably by @feliperodri in model-checking#3045
- Add
--use-local-toolchain
to Kani setup by @jaisnan in model-checking#3056 - Replace internal reverse_postorder by a stable one by @celinval in model-checking#3064
- Add option to override
--crate-name
fromkani
by @adpaco-aws in model-checking#3054 - Rust toolchain upgraded to 2024-03-11 by @adpaco-ws @celinval @zyadh
Full Changelog: https://github.com/model-checking/kani/compare/kani-0.47.0...kani-0.48.0
- Upgrade toolchain to 2024-02-14 by @zhassan-aws in model-checking#3036
Full Changelog: https://github.com/model-checking/kani/compare/kani-0.46.0...kani-0.47.0
modifies
Clauses for Function Contracts by @JustusAdam in model-checking#2800- Fix ICEs due to mismatched arguments by @celinval in model-checking#2994. Resolves the following issues:
- Enable powf*, exp*, log* intrinsics by @tautschnig in model-checking#2996
- Upgrade Rust toolchain to nightly-2024-01-24 by @celinval @feliperodri @qinheping
Full Changelog: https://github.com/model-checking/kani/compare/kani-0.45.0...kani-0.46.0
- Upgrade toolchain to nightly-2024-01-17 by @celinval in model-checking#2976
Full Changelog: https://github.com/model-checking/kani/compare/kani-0.44.0...kani-0.45.0
- Rust toolchain upgraded to
nightly-2024-01-08
by @adpaco-aws @celinval @zhassan-aws
Full Changelog: https://github.com/model-checking/kani/compare/kani-0.43.0...kani-0.44.0
- Rust toolchain upgraded to
nightly-2023-12-14
by @tautschnig and @adpaco-aws
Full Changelog: https://github.com/model-checking/kani/compare/kani-0.42.0...kani-0.43.0
- Build CBMC from source and install as package on non-x86_64 by @bennofs in model-checking#2877 and model-checking#2878
- Emit suggestions and an explanation when CBMC runs out of memory by @JustusAdam in model-checking#2885
- Rust toolchain upgraded to
nightly-2023-11-28
by @celinval
Full Changelog: https://github.com/model-checking/kani/compare/kani-0.41.0...kani-0.42.0
- Set minimum python to 3.7 in docker container and release action by @remi-delmas-3000 in model-checking#2879
- Delete
any_slice
which has been deprecated since Kani 0.38.0. by @zhassan-aws in model-checking#2860
- Make
cover
const by @jswrenn in model-checking#2867 - Change
expect()
from taking formatted strings to useunwrap_or_else()
by @matthiaskrgr in model-checking#2865 - Fix setup for
aarch64-unknown-linux-gnu
platform by @adpaco-aws in model-checking#2864 - Do not override
std
library during playback by @celinval in model-checking#2852 - Rust toolchain upgraded to
nightly-2023-11-11
by @zhassan-aws
Full Changelog: https://github.com/model-checking/kani/compare/kani-0.40.0...kani-0.41.0
- Ease setup in Amazon Linux 2 by @adpaco-aws in model-checking#2833
- Propagate backend options into goto-synthesizer by @qinheping in model-checking#2643
- Update CBMC version to 5.95.1 by @adpaco-aws in model-checking#2844
- Rust toolchain upgraded to
nightly-2023-10-31
by @jaisnan @adpaco-aws
Full Changelog: https://github.com/model-checking/kani/compare/kani-0.39.0...kani-0.40.0
- Limit --exclude to workspace packages by @tautschnig in model-checking#2808
- Fix panic warning and add arbitrary Duration by @celinval in model-checking#2820
- Update CBMC version to 5.94 by @celinval in model-checking#2821
- Rust toolchain upgraded to
nightly-2023-10-17
by @celinval @tautschnig
Full Changelog: https://github.com/model-checking/kani/compare/kani-0.38.0...kani-0.39.0
- Deprecate
any_slice
by @zhassan-aws in model-checking#2789
- Provide better error message for invalid stubs by @JustusAdam in model-checking#2787
- Simple Stubbing with Contracts by @JustusAdam in model-checking#2746
- Avoid mismatch when generating structs that represent scalar data but also include ZSTs by @adpaco-aws in model-checking#2794
- Prevent kani crash during setup for first time by @jaisnan in model-checking#2799
- Create concrete playback temp files in source directory by @tautschnig in model-checking#2804
- Bump CBMC version by @zhassan-aws in model-checking#2796
- Update Rust toolchain to 2023-09-23 by @tautschnig in model-checking#2806
Full Changelog: https://github.com/model-checking/kani/compare/kani-0.37.0...kani-0.38.0
- Delete obsolete stubs for
Vec
and related options by @zhassan-aws in model-checking#2770 - Add support for the ARM64 Linux platform by @adpaco-aws in model-checking#2757
- Function Contracts: Support for defining and checking
requires
andensures
clauses by @JustusAdam in model-checking#2655 - Force
any_vec
capacity to match length by @celinval in model-checking#2765 - Fix expected value for
pref_align_of
under aarch64/macos by @remi-delmas-3000 in model-checking#2782 - Bump CBMC version to 5.92.0 by @zhassan-aws in model-checking#2771
- Upgrade to Kissat 3.1.1 by @zhassan-aws in model-checking#2756
- Rust toolchain upgraded to
nightly-2023-09-19
by @remi-delmas-3000 @tautschnig
Full Changelog: https://github.com/model-checking/kani/compare/kani-0.36.0...kani-0.37.0
- Enable
-Z stubbing
and error out instead of ignoring stub by @celinval in model-checking#2678 - Enable concrete playback for failure of UB checks by @zhassan-aws in model-checking#2727
- Bump CBMC version to 5.91.0 by @adpaco-aws in model-checking#2733
- Rust toolchain upgraded to
nightly-2023-09-06
by @celinval @jaisnan @adpaco-aws
Full Changelog: https://github.com/model-checking/kani/compare/kani-0.35.0...kani-0.36.0
- Add support to
simd_bitmask
by @celinval in model-checking#2677 - Add integer overflow checking for
simd_div
andsimd_rem
by @reisnera in model-checking#2645 - Bump CBMC version by @zhassan-aws in model-checking#2702
- Upgrade Rust toolchain to 2023-08-19 by @zhassan-aws in model-checking#2696
Full Changelog: https://github.com/model-checking/kani/compare/kani-0.34.0...kani-0.35.0
- Change default solver to CaDiCaL by @celinval in model-checking#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.
- Allow specifying the scheduling strategy in #[kani_proof] for async functions by @fzaiser in model-checking#1661
- Support for stubbing out foreign functions by @feliperodri in model-checking#2658
- Coverage reporting without a need for cbmc-viewer by @adpaco-aws in model-checking#2609
- Add support to array-based SIMD by @celinval in model-checking#2633
- Add unchecked/SIMD bitshift checks and disable CBMC flag by @reisnera in model-checking#2630
- Fix codegen of constant byte slices to address spurious verification failures by @zhassan in model-checking#2663
- Bump CBMC to v5.89.0 by @remi-delmas-3000 in model-checking#2662
- Update Rust toolchain to nightly 2023-08-04 by @remi-delmas-3000 in model-checking#2661
Full Changelog: https://github.com/model-checking/kani/compare/kani-0.33.0...kani-0.34.0
- Add support for sysconf by @feliperodri in model-checking#2557
- Print Kani version by @adpaco-aws in model-checking#2619
- Upgrade Rust toolchain to nightly-2023-07-01 by @qinheping in model-checking#2616
- Bump CBMC version to 5.88.1 by @zhassan-aws in model-checking#2623
Full Changelog: https://github.com/model-checking/kani/compare/kani-0.32.0...kani-0.33.0
- Add kani::spawn and an executor to the Kani library by @fzaiser in model-checking#1659
- Add "kani" configuration key to enable conditional compilation in build scripts by @celinval in model-checking#2297
- Adds posix_memalign to the list of supported builtins by @feliperodri in model-checking#2601
- Upgrade rust toolchain to nightly-2023-06-20 by @celinval in model-checking#2551
- Update rust toolchain to 2023-06-22 by @celinval in model-checking#2588
- Automatic toolchain upgrade to nightly-2023-06-24 by @github-actions in model-checking#2600
- Bump CBMC version to 5.87.0 by @adpaco-aws in model-checking#2598
Full Changelog: https://github.com/model-checking/kani/compare/kani-0.31.0...kani-0.32.0
- Add
--exact
flag by @jaisnan in model-checking#2527 - Build the verification libraries using Kani compiler by @celinval in model-checking#2534
- Verify all Kani attributes in all crate items upfront by @celinval in model-checking#2536
- Update README.md - fix link locations for badge images in markdown by @phayes in model-checking#2537
- Bump CBMC version to 5.86.0 by @zhassan-aws in model-checking#2561
Full Changelog: https://github.com/model-checking/kani/compare/kani-0.30.0...kani-0.31.0
- Remove --harness requirement from stubbing by @celinval in model-checking#2495
- Add target selection for cargo kani by @celinval in model-checking#2507
- Generate Multiple playback harnesses when multiple crashes exist in a single harness. by @YoshikiTakashima in model-checking#2496
- Escape Zero-size types in playback by @YoshikiTakashima in model-checking#2508
- Do not crash when
rustfmt
fails. by @YoshikiTakashima in model-checking#2511 - De-duplicate same input injections for the same harness. by @YoshikiTakashima in model-checking#2513
- Update Cbmc version by @celinval in model-checking#2512
- Upgrade rust toolchain to 2023-04-30 by @zhassan-aws in model-checking#2456
Full Changelog: https://github.com/model-checking/kani/compare/kani-0.29.0...kani-0.30.0
- Create a playback command to make it easier to run Kani generated tests (pull request by @celinval)
- Fix symtab json file removal and reduce regression scope (pull request by @celinval)
- Fix regression on concrete playback inplace (pull request by @celinval)
- Fix static variable initialization when they have the same value (pull request by @celinval)
- Improve assess and regression time (pull request by @celinval)
- Fix playback with build scripts (pull request by @celinval)
- Delay printing playback harness until after verification status (pull request by @YoshikiTakashima)
- Update rust toolchain to 2023-04-29 (pull request by @zhassan-aws)
- Bump CBMC version to 5.84.0 (pull request by @tautschn)
Full Changelog: https://github.com/model-checking/kani/compare/kani-0.28.0...kani-0.29.0
- The unstable
--c-lib
option now requires-Z c-ffi
to enable C-FFI support by @celinval in model-checking#2425
- Enforce unstable APIs can only be used if the related feature is enabled by @celinval in model-checking#2386
- Get rid of the legacy mode by @celinval in model-checking#2427
- Limit FFI calls by default to explicitly supported ones by @celinval in model-checking#2428
- Fix the order of operands for generator structs by @zhassan-aws in model-checking#2436
- Add a few options to dump the reachability graph (debug only) by @celinval in model-checking#2433
- Perform reachability analysis on a per-harness basis by @celinval in model-checking#2439
- Bump CBMC version to 5.83.0 by @zhassan-aws in model-checking#2441
- Upgrade the toolchain to nightly-2023-04-16 by @celinval in model-checking#2406
Full Changelog: https://github.com/model-checking/kani/compare/kani-0.27.0...kani-0.28.0
- Allow excluding packages from verification with
--exclude
by @adpaco-aws in model-checking#2399 - Add size_of annotation to help CBMC's allocator by @tautschnig in model-checking#2395
- Implement
kani::Arbitrary
forBox<T>
by @adpaco-aws in model-checking#2404 - Use optimized overflow operation everywhere by @celinval in model-checking#2405
- Print compilation stats in verbose mode by @celinval in model-checking#2420
- Bump CBMC version to 5.82.0 by @adpaco-aws in model-checking#2417
Full Changelog: https://github.com/model-checking/kani/compare/kani-0.26.0...kani-0.27.0
- The Kani reference now includes an "Attributes" section that describes each of the attributes available in Kani (pull request by @adpaco-aws)
- Users' choice of SAT solver, specified by the
solver
attribute, is now propagated to the loop-contract synthesizer (pull request by @qinheping) - Unit tests generated by the concrete playback feature now compile correctly when using
RUSTFLAGS="--cfg=kani"
(pull request by @jaisnan) - The Rust toolchain is updated to 2023-02-18 (pull request by @tautschnig)
Full Changelog: https://github.com/model-checking/kani/compare/kani-0.25.0...kani-0.26.0
- Add implementation for the
#[kani::should_panic]
attribute by @adpaco-aws in model-checking#2315 - Upgrade Rust toolchain to nightly-2023-02-04 by @tautschnig in model-checking#2324
- Bump CBMC version to 5.80.0 by @zhassan-aws in model-checking#2336
Full Changelog: https://github.com/model-checking/kani/compare/kani-0.24.0...kani-0.25.0
- Remove the second parameter in the
kani::any_where
function by @zhassan-aws in #2257 We removed the second parameter in thekani::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);
- 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.