Bump Kani version to 0.53.0

CHANGELOG.md

@@ -4,6 +4,44 @@ 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.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 the next release once remaining performance issues have been resolved.
+
+### What's Changed
+
+* Add `kani_core` library placeholder and build logic by @celinval in https://github.com/model-checking/kani/pull/3227
+* Change ensures into closures by @pi314mm in https://github.com/model-checking/kani/pull/3207
+* (Re)introduce `Invariant` trait by @adpaco-aws in https://github.com/model-checking/kani/pull/3190
+* Remove empty box creation from contracts impl by @celinval in https://github.com/model-checking/kani/pull/3233
+* Add a new verify-std subcommand to Kani by @celinval in https://github.com/model-checking/kani/pull/3231
+* Inject pointer validity check when casting raw pointers to references by @artemagvanian in https://github.com/model-checking/kani/pull/3221
+* Do not turn trivially diverging loops into assume(false) by @tautschnig in https://github.com/model-checking/kani/pull/3223
+* Fix "unused mut" warnings created by generated code. by @jsalzbergedu in https://github.com/model-checking/kani/pull/3247
+* Refactor stubbing so Kani compiler only invoke rustc once per crate by @celinval in https://github.com/model-checking/kani/pull/3245
+* Use cfg=kani_host for host crates by @tautschnig in https://github.com/model-checking/kani/pull/3244
+* Add intrinsics and Arbitrary support for no_core by @jaisnan in https://github.com/model-checking/kani/pull/3230
+* Fix a few issues with std verification by @celinval in https://github.com/model-checking/kani/pull/3255
+* Fix contract of constant fn with effect feature by @celinval in https://github.com/model-checking/kani/pull/3259
+* Fix a few more issues with the std library by @celinval in https://github.com/model-checking/kani/pull/3261
+* Fix typed_swap for ZSTs by @tautschnig in https://github.com/model-checking/kani/pull/3256
+* Remove further uses of Location::none by @tautschnig in https://github.com/model-checking/kani/pull/3253
+* Add a `#[derive(Invariant)]` macro by @adpaco-aws in https://github.com/model-checking/kani/pull/3250
+* Contracts: History Expressions via "old" monad by @pi314mm in https://github.com/model-checking/kani/pull/3232
+* Function Contracts: remove instances of _renamed by @pi314mm in https://github.com/model-checking/kani/pull/3274
+* Remove support for the unstable argument `--function` by @celinval in https://github.com/model-checking/kani/pull/3278
+* Deprecate `--visualize` in favor of concrete playback by @celinval in https://github.com/model-checking/kani/pull/3281
+* Fix operand in fat pointer comparison by @pi314mm in https://github.com/model-checking/kani/pull/3297
+* C library: declare malloc by @tautschnig in https://github.com/model-checking/kani/pull/3296
+* Function Contracts: Closure Type Inference by @pi314mm in https://github.com/model-checking/kani/pull/3307
+* Add support for f16 and f128 for toolchain upgrade to 6/28 by @jaisnan in https://github.com/model-checking/kani/pull/3306
+* Towards Proving Memory Initialization by @artemagvanian in https://github.com/model-checking/kani/pull/3264
+* Rust toolchain upgraded to `nightly-2024-07-01` by @tautschnig @celinval @jaisnan @adpaco-aws
+
+**Full Changelog**: https://github.com/model-checking/kani/compare/kani-0.52.0...kani-0.53.0
+
 ## [0.52.0]
 
 ## What's Changed

Cargo.lock

@@ -92,7 +92,7 @@ checksum = "b048fb63fd8b5923fc5aa7b340d8e156aec7ec02f0c78fa8a6ddc2613f6f71de"
 
 [[package]]
 name = "build-kani"
-version = "0.52.0"
+version = "0.53.0"
 dependencies = [
  "anyhow",
  "cargo_metadata",
@@ -228,7 +228,7 @@ dependencies = [
 
 [[package]]
 name = "cprover_bindings"
-version = "0.52.0"
+version = "0.53.0"
 dependencies = [
  "lazy_static",
  "linear-map",
@@ -405,14 +405,14 @@ checksum = "49f1f14873335454500d59611f1cf4a4b0f786f9ac11f4312a78e4cf2566695b"
 
 [[package]]
 name = "kani"
-version = "0.52.0"
+version = "0.53.0"
 dependencies = [
  "kani_macros",
 ]
 
 [[package]]
 name = "kani-compiler"
-version = "0.52.0"
+version = "0.53.0"
 dependencies = [
  "clap",
  "cprover_bindings",
@@ -433,7 +433,7 @@ dependencies = [
 
 [[package]]
 name = "kani-driver"
-version = "0.52.0"
+version = "0.53.0"
 dependencies = [
  "anyhow",
  "cargo_metadata",
@@ -461,7 +461,7 @@ dependencies = [
 
 [[package]]
 name = "kani-verifier"
-version = "0.52.0"
+version = "0.53.0"
 dependencies = [
  "anyhow",
  "home",
@@ -470,14 +470,14 @@ dependencies = [
 
 [[package]]
 name = "kani_core"
-version = "0.52.0"
+version = "0.53.0"
 dependencies = [
  "kani_macros",
 ]
 
 [[package]]
 name = "kani_macros"
-version = "0.52.0"
+version = "0.53.0"
 dependencies = [
  "proc-macro-error",
  "proc-macro2",
@@ -487,7 +487,7 @@ dependencies = [
 
 [[package]]
 name = "kani_metadata"
-version = "0.52.0"
+version = "0.53.0"
 dependencies = [
  "clap",
  "cprover_bindings",
@@ -992,7 +992,7 @@ checksum = "3c5e1a9a646d36c3599cd173a41282daf47c44583ad367b8e6837255952e5c67"
 
 [[package]]
 name = "std"
-version = "0.52.0"
+version = "0.53.0"
 dependencies = [
  "kani",
 ]

Cargo.toml

@@ -3,7 +3,7 @@
 
 [package]
 name = "kani-verifier"
-version = "0.52.0"
+version = "0.53.0"
 edition = "2021"
 description = "A bit-precise model checker for Rust."
 readme = "README.md"

cprover_bindings/Cargo.toml

@@ -3,7 +3,7 @@
 
 [package]
 name = "cprover_bindings"
-version = "0.52.0"
+version = "0.53.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false

kani-compiler/Cargo.toml

@@ -3,7 +3,7 @@
 
 [package]
 name = "kani-compiler"
-version = "0.52.0"
+version = "0.53.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false

kani-driver/Cargo.toml

@@ -3,7 +3,7 @@
 
 [package]
 name = "kani-driver"
-version = "0.52.0"
+version = "0.53.0"
 edition = "2021"
 description = "Build a project with Kani and run all proof harnesses"
 license = "MIT OR Apache-2.0"

kani_metadata/Cargo.toml

@@ -3,7 +3,7 @@
 
 [package]
 name = "kani_metadata"
-version = "0.52.0"
+version = "0.53.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false

library/kani/Cargo.toml

@@ -3,7 +3,7 @@
 
 [package]
 name = "kani"
-version = "0.52.0"
+version = "0.53.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false

library/kani_core/Cargo.toml

@@ -3,7 +3,7 @@
 
 [package]
 name = "kani_core"
-version = "0.52.0"
+version = "0.53.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false

library/kani_macros/Cargo.toml

@@ -3,7 +3,7 @@
 
 [package]
 name = "kani_macros"
-version = "0.52.0"
+version = "0.53.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false

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.52.0"
+version = "0.53.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false

tools/build-kani/Cargo.toml

@@ -3,7 +3,7 @@
 
 [package]
 name = "build-kani"
-version = "0.52.0"
+version = "0.53.0"
 edition = "2021"
 description = "Builds Kani, Sysroot and release bundle."
 license = "MIT OR Apache-2.0"