Skip to content

Latest commit

 

History

History
551 lines (403 loc) · 35.2 KB

CHANGELOG.md

File metadata and controls

551 lines (403 loc) · 35.2 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.57.0]

Major Changes

Breaking Changes

What's Changed

  • Remove the overflow checks for wrapping_offset by @zhassan-aws in model-checking#3589
  • Support fully-qualified --package arguments by @celinval in model-checking#3593
  • Implement proper function pointer handling for validity checks by @celinval in model-checking#3606
  • Add fn that checks pointers point to same allocation by @celinval in model-checking#3583
  • [Lean back-end] Preserve variable names by @zhassan-aws in model-checking#3560
  • Emit an error when proof_for_contract function is not found by @zhassan-aws in model-checking#3609
  • [Lean back-end] Rename user-facing options from Aeneas to Lean by @zhassan-aws in model-checking#3630
  • Fix ICE due to mishandling of Aggregate rvalue for raw pointers to trait objects by @carolynzech in model-checking#3636
  • Fix loop contracts transformation when loops in branching by @qinheping in model-checking#3640
  • Move any_slice_from_array to kani_core by @qinheping in model-checking#3646
  • Implement Arbitrary for Range* by @c410-f3r in model-checking#3666
  • Add support for float_to_int_unchecked by @zhassan-aws in model-checking#3660
  • Change same_allocation to accept wide pointers by @celinval in model-checking#3684
  • Derive Arbitrary for enums with a single variant by @AlgebraicWolf in model-checking#3692
  • Apply loop contracts only if there exists some usage by @qinheping in model-checking#3694
  • Add support for f16 and f128 in float_to_int_unchecked intrinsic by @zhassan-aws in model-checking#3701
  • Fix codegen for rvalue aggregate raw pointer to an adt with slice tail by @carolynzech in model-checking#3644
  • Improve Kani handling of function markers by @celinval in model-checking#3718
  • Enable contracts for const generic functions by @qinheping in model-checking#3726
  • List Subcommand Improvements by @carolynzech in model-checking#3729
  • [Lean back-end] add support for enum, struct, tuple in llbc backend by @thanhnguyen-aws in model-checking#3721
  • Fix issues with how we compute DST size by @celinval in model-checking#3687
  • Fix size and alignment computation for intrinsics by @celinval in model-checking#3734
  • Add a Kani function that checks if the range of a float is valid for conversion to int by @zhassan-aws in model-checking#3742
  • Add out of bounds check for offset intrinsics by @celinval in model-checking#3755
  • Automatic upgrade of CBMC from 6.3.1 to 6.4.1
  • Rust toolchain upgraded to nightly-2024-12-15 by @zhassan-aws @carolynzech @qinheping @celinval @tautschnig

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.56.0...kani-0.57.0

[0.56.0]

Major/Breaking Changes

What's Changed

  • Enable stubbing and function contracts for primitive types by @celinval in model-checking#3496
  • Instrument validity checks for pointer to reference casts for slices and str's by @zhassan-aws in model-checking#3513
  • Fail compilation if proof_for_contract is added to generic function by @carolynzech in model-checking#3522
  • Fix storing coverage data in cargo projects by @adpaco-aws in model-checking#3527
  • Add experimental API to generate arbitrary pointers by @celinval in model-checking#3538
  • Running verify-std no longer changes Cargo files by @celinval in model-checking#3577
  • Add an LLBC backend by @zhassan-aws in model-checking#3514
  • Fix the computation of the number of bytes of a pointer offset by @zhassan-aws in model-checking#3584
  • Rust toolchain upgraded to nightly-2024-10-03 by @qinheping @tautschnig @celinval
  • CBMC upgraded to 6.3.1 by @tautschnig in model-checking#3537

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

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