Skip to content

Latest commit

 

History

History
482 lines (345 loc) · 29.4 KB

CHANGELOG.md

File metadata and controls

482 lines (345 loc) · 29.4 KB
Raw

Changelog

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.

[0.55.0]

Major/Breaking Changes

  • Coverage reporting in Kani is now source-based instead of line-based. Consequently, the unstable -Zline-coverage flag has been replaced with a -Zsource-coverage one. Check the Source-Coverage RFC for more details.
  • Several improvements were made to the memory initialization checks. The current state is summarized in model-checking#3300. We welcome your feedback!

What's Changed

  • Update CBMC build instructions for Amazon Linux 2 by @tautschnig in model-checking#3431
  • Implement memory initialization state copy functionality by @artemagvanian in model-checking#3350
  • Make points-to analysis handle all intrinsics explicitly by @artemagvanian in model-checking#3452
  • Avoid corner-cases by grouping instrumentation into basic blocks and using backward iteration by @artemagvanian in model-checking#3438
  • Fix ICE due to mishandling of Aggregate rvalue for raw pointers to str by @celinval in model-checking#3448
  • Basic support for memory initialization checks for unions by @artemagvanian in model-checking#3444
  • Adopt Rust's source-based code coverage instrumentation by @adpaco-aws in model-checking#3119
  • Extra tests and bug fixes to the delayed UB instrumentation by @artemagvanian in model-checking#3419
  • Partially integrate uninit memory checks into verify_std by @artemagvanian in model-checking#3470
  • Rust toolchain upgraded to nightly-2024-09-03 by @jaisnan @carolynzech

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.54.0...kani-0.55.0

[0.54.0]

Major Changes

  • We added support for slices in the #[kani::modifies(...)] clauses when using function contracts.
  • We introduce an #[safety_constraint(...)] attribute helper for the Arbitrary and Invariant macros.
  • We enabled support for concrete playback for harness that contains stubs or function contracts.
  • We added support for log2*, log10*, powif*, fma*, and sqrt* intrisincs.

Breaking Changes

  • The -Z ptr-to-ref-cast-checks option has been removed, and pointer validity checks when casting raw pointers to references are now run by default.

What's Changed

New Contributors

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.53.0...kani-0.54.0

[0.53.0]

Major Changes

  • The --visualize option is being deprecated and will be removed in a future release. Consider using the --concrete-playback option instead.
  • The -Z ptr-to-ref-cast-checks option is being introduced to check pointer validity when casting raw pointers to references. The feature is currently behind an unstable flag but is expected to be stabilized in a future release once remaining performance issues have been resolved.
  • The -Z uninit-checks option is being introduced to check memory initialization. The feature is currently behind an unstable flag and also requires the -Z ghost-state option.

Breaking Changes

What's Changed

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.52.0...kani-0.53.0

[0.52.0]

What's Changed

  • New section about linter configuraton checking in the doc by @remi-delmas-3000 in model-checking#3198
  • Fix {,e}println!() by @GrigorenkoPV in model-checking#3209
  • Contracts for a few core functions by @celinval in model-checking#3107
  • Add simple API for shadow memory by @zhassan-aws in model-checking#3200
  • Upgrade Rust toolchain to 2024-05-28 by @zhassan-aws @remi-delmas-3000 @qinheping

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.51.0...kani-0.52.0

[0.51.0]

What's Changed

  • Do not assume that ZST-typed symbols refer to unique objects by @tautschnig in model-checking#3134
  • Remove kani::Arbitrary from the modifies 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

[0.50.0]

Major Changes

What's Changed

  • 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

[0.49.0]

What's Changed

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.48.0...kani-0.49.0

[0.48.0]

Major Changes

  • We fixed a soundness bug that in some cases may cause Kani to not detect a use-after-free issue in model-checking#3063

What's Changed

  • Fix codegen_atomic_binop for atomic_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 from kani 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

[0.47.0]

What's Changed

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.46.0...kani-0.47.0

[0.46.0]

What's Changed

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.45.0...kani-0.46.0

[0.45.0]

What's Changed

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.44.0...kani-0.45.0

[0.44.0]

What's Changed

  • 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

[0.43.0]

What's Changed

  • 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

[0.42.0]

What's Changed

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.41.0...kani-0.42.0

[0.41.0]

Breaking Changes

  • 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

What's Changed

  • Make cover const by @jswrenn in model-checking#2867
  • Change expect() from taking formatted strings to use unwrap_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

[0.40.0]

What's Changed

  • 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

[0.39.0]

What's Changed

  • 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

[0.38.0]

Major Changes

What's Changed

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.37.0...kani-0.38.0

[0.37.0]

Major Changes

What's Changed

  • Function Contracts: Support for defining and checking requires and ensures 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

[0.36.0]

What's Changed

  • 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

[0.35.0]

What's Changed

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.34.0...kani-0.35.0

[0.34.0]

Breaking Changes

  • 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.

What's Changed

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.33.0...kani-0.34.0

[0.33.0]

What's Changed

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.32.0...kani-0.33.0

[0.32.0]

What's Changed

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.31.0...kani-0.32.0

[0.31.0]

What's Changed

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.30.0...kani-0.31.0

[0.30.0]

What's Changed

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.29.0...kani-0.30.0

[0.29.0]

Major Changes

  • Create a playback command to make it easier to run Kani generated tests (pull request by @celinval)

What Else has Changed

  • 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

[0.28.0]

Breaking Changes

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

What's Changed

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.27.0...kani-0.28.0

[0.27.0]

What's Changed

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.26.0...kani-0.27.0

[0.26.0]

What's Changed

  • 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

[0.25.0]

What's Changed

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.24.0...kani-0.25.0

[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.