diff --git a/CHANGELOG.md b/CHANGELOG.md index b8b95786ec9d..9a6b5598a8b1 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -4,6 +4,41 @@ This file contains notable changes (e.g. breaking changes, major changes, etc.) This file was introduced starting Kani 0.23.0, so it only contains changes from version 0.23.0 onwards. +## [0.63.0] + +### Breaking Changes +* Finish deprecating `--enable-unstable`, `--restrict-vtable`, and `--write-json-symtab` by @carolynzech in https://github.com/model-checking/kani/pull/4110 + +### Major Changes +* Add support for quantifiers by @qinheping in https://github.com/model-checking/kani/pull/3993 + +### What's Changed +* Improvements to autoharness feature: + * Autoharness argument validation: only error on `--quiet` if `--list` was passed by @carolynzech in https://github.com/model-checking/kani/pull/4069 + * Autoharness: change `pattern` options to accept regexes by @carolynzech in https://github.com/model-checking/kani/pull/4144 +* Target feature changes: + * Enable target features: x87 and sse2 by @thanhnguyen-aws in https://github.com/model-checking/kani/pull/4062 + * Set target features depending on the target architecture by @zhassan-aws in https://github.com/model-checking/kani/pull/4127 +* Support for quantifiers: + * Fix the error that Kani panics when there is no external parameter in quantifier's closure. by @thanhnguyen-aws in https://github.com/model-checking/kani/pull/4088 + * Gate quantifiers behind an experimental feature by @thanhnguyen-aws in https://github.com/model-checking/kani/pull/4141 +* Other: + * Fix the bug: Loop contracts are not composable with function contracts by @thanhnguyen-aws in https://github.com/model-checking/kani/pull/3979 + * Add setup scripts for Ubuntu 20.04 by @zhassan-aws in https://github.com/model-checking/kani/pull/4082 + * Use our toolchain when invoking `cargo metadata` by @carolynzech in https://github.com/model-checking/kani/pull/4090 + * Fix a bug codegening `SwitchInt`s with only an otherwise branch by @bkirwi in https://github.com/model-checking/kani/pull/4095 + * Update `kani::mem` pointer validity documentation by @carolynzech in https://github.com/model-checking/kani/pull/4092 + * Add support for edition 2018 crates using assert! (Fixes #3717) by @sintemal in https://github.com/model-checking/kani/pull/4096 + * Handle generic defaults in BoundedArbitrary derives by @zhassan-aws in https://github.com/model-checking/kani/pull/4117 + * `ty_mangled_name`: only use non-mangled name if `-Zcffi` is enabled. by @carolynzech in https://github.com/model-checking/kani/pull/4114 + * Improve Help Menu by @carolynzech in https://github.com/model-checking/kani/pull/4109 + * Start stabilizing `--jobs` and `list`; deprecate default memory checks by @carolynzech in https://github.com/model-checking/kani/pull/4108 + * Refactor simd_bitmask to reduce the number of iterations by @zhassan-aws in https://github.com/model-checking/kani/pull/4129 + * Improve linking error output for `#[no_std]` crates by @AlexanderPortland in https://github.com/model-checking/kani/pull/4126 + * Rust toolchain upgraded to 2025-06-03 by @carolynzech @thanhnguyen-aws @zhassan-aws + +**Full Changelog**: https://github.com/model-checking/kani/compare/kani-0.62.0...kani-0.63.0 + ## [0.62.0] ### What's Changed diff --git a/Cargo.lock b/Cargo.lock index d9afd9fa7d0b..31107efb4cb6 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -182,7 +182,7 @@ dependencies = [ [[package]] name = "build-kani" -version = "0.62.0" +version = "0.63.0" dependencies = [ "anyhow", "cargo_metadata", @@ -404,7 +404,7 @@ dependencies = [ [[package]] name = "cprover_bindings" -version = "0.62.0" +version = "0.63.0" dependencies = [ "lazy_static", "linear-map", @@ -973,7 +973,7 @@ checksum = "72167d68f5fce3b8655487b8038691a3c9984ee769590f93f2a631f4ad64e4f5" [[package]] name = "kani" -version = "0.62.0" +version = "0.63.0" dependencies = [ "kani_core", "kani_macros", @@ -981,7 +981,7 @@ dependencies = [ [[package]] name = "kani-compiler" -version = "0.62.0" +version = "0.63.0" dependencies = [ "charon", "clap", @@ -1018,7 +1018,7 @@ dependencies = [ [[package]] name = "kani-driver" -version = "0.62.0" +version = "0.63.0" dependencies = [ "anyhow", "cargo_metadata", @@ -1047,7 +1047,7 @@ dependencies = [ [[package]] name = "kani-verifier" -version = "0.62.0" +version = "0.63.0" dependencies = [ "anyhow", "home", @@ -1056,14 +1056,14 @@ dependencies = [ [[package]] name = "kani_core" -version = "0.62.0" +version = "0.63.0" dependencies = [ "kani_macros", ] [[package]] name = "kani_macros" -version = "0.62.0" +version = "0.63.0" dependencies = [ "proc-macro-error2", "proc-macro2", @@ -1073,7 +1073,7 @@ dependencies = [ [[package]] name = "kani_metadata" -version = "0.62.0" +version = "0.63.0" dependencies = [ "clap", "cprover_bindings", @@ -1883,7 +1883,7 @@ dependencies = [ [[package]] name = "std" -version = "0.62.0" +version = "0.63.0" dependencies = [ "kani", ] diff --git a/Cargo.toml b/Cargo.toml index 455ee300bfef..11b3337cd77a 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-verifier" -version = "0.62.0" +version = "0.63.0" edition = "2021" description = "A bit-precise model checker for Rust." readme = "README.md" diff --git a/cprover_bindings/Cargo.toml b/cprover_bindings/Cargo.toml index 641d7862d776..0c876bc6c722 100644 --- a/cprover_bindings/Cargo.toml +++ b/cprover_bindings/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "cprover_bindings" -version = "0.62.0" +version = "0.63.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml index b4193cec36d7..3650276d39a5 100644 --- a/kani-compiler/Cargo.toml +++ b/kani-compiler/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-compiler" -version = "0.62.0" +version = "0.63.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml index afd9acff9c65..e3f75f00e063 100644 --- a/kani-driver/Cargo.toml +++ b/kani-driver/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-driver" -version = "0.62.0" +version = "0.63.0" edition = "2021" description = "Build a project with Kani and run all proof harnesses" license = "MIT OR Apache-2.0" diff --git a/kani_metadata/Cargo.toml b/kani_metadata/Cargo.toml index 73eee459900d..784589f53ba6 100644 --- a/kani_metadata/Cargo.toml +++ b/kani_metadata/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani_metadata" -version = "0.62.0" +version = "0.63.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/kani/Cargo.toml b/library/kani/Cargo.toml index 71fc4275a606..5d0f28d04b5e 100644 --- a/library/kani/Cargo.toml +++ b/library/kani/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani" -version = "0.62.0" +version = "0.63.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/kani_core/Cargo.toml b/library/kani_core/Cargo.toml index bd824f0e1c97..d20c6dab029a 100644 --- a/library/kani_core/Cargo.toml +++ b/library/kani_core/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani_core" -version = "0.62.0" +version = "0.63.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/kani_macros/Cargo.toml b/library/kani_macros/Cargo.toml index ccb88d4fb098..47fef21b6896 100644 --- a/library/kani_macros/Cargo.toml +++ b/library/kani_macros/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani_macros" -version = "0.62.0" +version = "0.63.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/std/Cargo.toml b/library/std/Cargo.toml index 724a4abca104..504928c471d3 100644 --- a/library/std/Cargo.toml +++ b/library/std/Cargo.toml @@ -5,7 +5,7 @@ # Note: this package is intentionally named std to make sure the names of # standard library symbols are preserved name = "std" -version = "0.62.0" +version = "0.63.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/tools/build-kani/Cargo.toml b/tools/build-kani/Cargo.toml index 7e7a971da0bc..2c07f6ffd4d7 100644 --- a/tools/build-kani/Cargo.toml +++ b/tools/build-kani/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "build-kani" -version = "0.62.0" +version = "0.63.0" edition = "2021" description = "Builds Kani, Sysroot and release bundle." license = "MIT OR Apache-2.0"