Skip to content

Latest commit

 

History

History
264 lines (183 loc) · 15.3 KB

CHANGELOG.md

File metadata and controls

264 lines (183 loc) · 15.3 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.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.