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"