Skip to content

Latest commit

 

History

History
247 lines (172 loc) · 14.4 KB

CHANGELOG.md

File metadata and controls

247 lines (172 loc) · 14.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.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.