From e004eccab617546526ab696511c99f7f957f6074 Mon Sep 17 00:00:00 2001 From: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> Date: Wed, 13 Mar 2024 15:54:31 -0700 Subject: [PATCH] Bump Kani version to 0.48.0 (#3075) These are the original release notes for the reference: ## What's Changed * Automatic cargo update to 2024-02-26 by @github-actions in https://github.com/model-checking/kani/pull/3043 * Upgrade rust toolchain to 2024-02-17 by @celinval in https://github.com/model-checking/kani/pull/3040 * Upgrade `windows-targets` crate to version 0.52.4 by @adpaco-aws in https://github.com/model-checking/kani/pull/3049 * Fix `codegen_atomic_binop` for `atomic_ptr` by @qinheping in https://github.com/model-checking/kani/pull/3047 * Upgrade Rust toolchain to `nightly-2024-02-25` by @adpaco-aws in https://github.com/model-checking/kani/pull/3048 * Update s2n-quic submodule by @zhassan-aws in https://github.com/model-checking/kani/pull/3050 * Update s2n-quic submodule weekly through dependabot by @zhassan-aws in https://github.com/model-checking/kani/pull/3053 * Retrieve info for recursion tracker reliably by @feliperodri in https://github.com/model-checking/kani/pull/3045 * Automatic cargo update to 2024-03-04 by @github-actions in https://github.com/model-checking/kani/pull/3055 * Upgrade Rust toolchain to `nightly-2024-03-01` by @adpaco-aws in https://github.com/model-checking/kani/pull/3052 * Add `--use-local-toolchain` to Kani setup by @jaisnan in https://github.com/model-checking/kani/pull/3056 * Replace internal reverse_postorder by a stable one by @celinval in https://github.com/model-checking/kani/pull/3064 * Add option to override `--crate-name` from `kani` by @adpaco-aws in https://github.com/model-checking/kani/pull/3054 * cargo update and fix macos CI by @zhassan-aws in https://github.com/model-checking/kani/pull/3067 * Bump tests/perf/s2n-quic from `d103836` to `1a7faa8` by @dependabot in https://github.com/model-checking/kani/pull/3066 * Upgrade toolchain to 2024-03-11 by @zhassan-aws in https://github.com/model-checking/kani/pull/3071 * Emit `dead` goto-instructions on MIR StatementDead by @karkhaz in https://github.com/model-checking/kani/pull/3063 **Full Changelog**: https://github.com/model-checking/kani/compare/kani-0.47.0...kani-0.48.0 --- CHANGELOG.md | 15 +++++++++++++++ Cargo.lock | 18 +++++++++--------- Cargo.toml | 2 +- cprover_bindings/Cargo.toml | 2 +- kani-compiler/Cargo.toml | 2 +- kani-driver/Cargo.toml | 2 +- kani_metadata/Cargo.toml | 2 +- library/kani/Cargo.toml | 2 +- library/kani_macros/Cargo.toml | 2 +- library/std/Cargo.toml | 2 +- tools/build-kani/Cargo.toml | 2 +- 11 files changed, 33 insertions(+), 18 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 968906b6f4b5..08f687d8e31c 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -4,6 +4,21 @@ 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.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 https://github.com/model-checking/kani/pull/3063 + +### What's Changed +* Fix `codegen_atomic_binop` for `atomic_ptr` by @qinheping in https://github.com/model-checking/kani/pull/3047 +* Retrieve info for recursion tracker reliably by @feliperodri in https://github.com/model-checking/kani/pull/3045 +* Add `--use-local-toolchain` to Kani setup by @jaisnan in https://github.com/model-checking/kani/pull/3056 +* Replace internal reverse_postorder by a stable one by @celinval in https://github.com/model-checking/kani/pull/3064 +* Add option to override `--crate-name` from `kani` by @adpaco-aws in https://github.com/model-checking/kani/pull/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 diff --git a/Cargo.lock b/Cargo.lock index 4db35ee6ab77..7009622b1733 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -141,7 +141,7 @@ dependencies = [ [[package]] name = "build-kani" -version = "0.47.0" +version = "0.48.0" dependencies = [ "anyhow", "cargo_metadata", @@ -292,7 +292,7 @@ dependencies = [ [[package]] name = "cprover_bindings" -version = "0.47.0" +version = "0.48.0" dependencies = [ "lazy_static", "linear-map", @@ -472,14 +472,14 @@ checksum = "b1a46d1a171d865aa5f83f92695765caa047a9b4cbae2cbf37dbd613a793fd4c" [[package]] name = "kani" -version = "0.47.0" +version = "0.48.0" dependencies = [ "kani_macros", ] [[package]] name = "kani-compiler" -version = "0.47.0" +version = "0.48.0" dependencies = [ "clap 4.5.2", "cprover_bindings", @@ -500,7 +500,7 @@ dependencies = [ [[package]] name = "kani-driver" -version = "0.47.0" +version = "0.48.0" dependencies = [ "anyhow", "cargo_metadata", @@ -528,7 +528,7 @@ dependencies = [ [[package]] name = "kani-verifier" -version = "0.47.0" +version = "0.48.0" dependencies = [ "anyhow", "clap 2.34.0", @@ -538,7 +538,7 @@ dependencies = [ [[package]] name = "kani_macros" -version = "0.47.0" +version = "0.48.0" dependencies = [ "proc-macro-error", "proc-macro2", @@ -548,7 +548,7 @@ dependencies = [ [[package]] name = "kani_metadata" -version = "0.47.0" +version = "0.48.0" dependencies = [ "clap 4.5.2", "cprover_bindings", @@ -1079,7 +1079,7 @@ checksum = "e6ecd384b10a64542d77071bd64bd7b231f4ed5940fba55e98c3de13824cf3d7" [[package]] name = "std" -version = "0.47.0" +version = "0.48.0" dependencies = [ "kani", ] diff --git a/Cargo.toml b/Cargo.toml index 845751118363..c863ffdc1945 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-verifier" -version = "0.47.0" +version = "0.48.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 3882e5ad300c..b9d0259b3577 100644 --- a/cprover_bindings/Cargo.toml +++ b/cprover_bindings/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "cprover_bindings" -version = "0.47.0" +version = "0.48.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml index c5ac44d0be1e..a5b7fd006180 100644 --- a/kani-compiler/Cargo.toml +++ b/kani-compiler/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-compiler" -version = "0.47.0" +version = "0.48.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml index a009f444840b..36a979a1366d 100644 --- a/kani-driver/Cargo.toml +++ b/kani-driver/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-driver" -version = "0.47.0" +version = "0.48.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 92cba41e27f8..6b6db72f4a6d 100644 --- a/kani_metadata/Cargo.toml +++ b/kani_metadata/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani_metadata" -version = "0.47.0" +version = "0.48.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/kani/Cargo.toml b/library/kani/Cargo.toml index 27fc6fc9ad6d..4da7f91a9ed7 100644 --- a/library/kani/Cargo.toml +++ b/library/kani/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani" -version = "0.47.0" +version = "0.48.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 46b6cf3daadd..b2254b5c8954 100644 --- a/library/kani_macros/Cargo.toml +++ b/library/kani_macros/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani_macros" -version = "0.47.0" +version = "0.48.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/std/Cargo.toml b/library/std/Cargo.toml index bdd10673f640..29467fddf70b 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.47.0" +version = "0.48.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 8c80063d7ff5..b75c373655bd 100644 --- a/tools/build-kani/Cargo.toml +++ b/tools/build-kani/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "build-kani" -version = "0.47.0" +version = "0.48.0" edition = "2021" description = "Builds Kani, Sysroot and release bundle." license = "MIT OR Apache-2.0"