From b88debb7e484039ecd8e99490bcb1e18e2a9da05 Mon Sep 17 00:00:00 2001 From: Kareem Khazem Date: Sat, 17 Jun 2023 03:12:22 +0100 Subject: [PATCH] Bump Kani version to 0.30.0 (#2529) Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> Co-authored-by: Celina G. Val --- 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 c0e718ca05e8..2252091e688b 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.30.0] + +## What's Changed +* Remove --harness requirement from stubbing by @celinval in https://github.com/model-checking/kani/pull/2495 +* Add target selection for cargo kani by @celinval in https://github.com/model-checking/kani/pull/2507 +* Generate Multiple playback harnesses when multiple crashes exist in a single harness. by @YoshikiTakashima in https://github.com/model-checking/kani/pull/2496 +* Escape Zero-size types in playback by @YoshikiTakashima in https://github.com/model-checking/kani/pull/2508 +* Do not crash when `rustfmt` fails. by @YoshikiTakashima in https://github.com/model-checking/kani/pull/2511 +* De-duplicate same input injections for the same harness. by @YoshikiTakashima in https://github.com/model-checking/kani/pull/2513 +* Update Cbmc version by @celinval in https://github.com/model-checking/kani/pull/2512 +* Upgrade rust toolchain to 2023-04-30 by @zhassan-aws in https://github.com/model-checking/kani/pull/2456 + +**Full Changelog**: https://github.com/model-checking/kani/compare/kani-0.29.0...kani-0.30.0 + + ## [0.29.0] ### Major Changes diff --git a/Cargo.lock b/Cargo.lock index 640e494ca704..f80547d4edcd 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -125,7 +125,7 @@ dependencies = [ [[package]] name = "build-kani" -version = "0.29.0" +version = "0.30.0" dependencies = [ "anyhow", "cargo_metadata", @@ -270,7 +270,7 @@ dependencies = [ [[package]] name = "cprover_bindings" -version = "0.29.0" +version = "0.30.0" dependencies = [ "lazy_static", "linear-map", @@ -514,14 +514,14 @@ checksum = "453ad9f582a441959e5f0d088b02ce04cfe8d51a8eaf077f12ac6d3e94164ca6" [[package]] name = "kani" -version = "0.29.0" +version = "0.30.0" dependencies = [ "kani_macros", ] [[package]] name = "kani-compiler" -version = "0.29.0" +version = "0.30.0" dependencies = [ "atty", "clap", @@ -544,7 +544,7 @@ dependencies = [ [[package]] name = "kani-driver" -version = "0.29.0" +version = "0.30.0" dependencies = [ "anyhow", "atty", @@ -573,7 +573,7 @@ dependencies = [ [[package]] name = "kani-verifier" -version = "0.29.0" +version = "0.30.0" dependencies = [ "anyhow", "home", @@ -582,7 +582,7 @@ dependencies = [ [[package]] name = "kani_macros" -version = "0.29.0" +version = "0.30.0" dependencies = [ "proc-macro-error", "proc-macro2", @@ -592,7 +592,7 @@ dependencies = [ [[package]] name = "kani_metadata" -version = "0.29.0" +version = "0.30.0" dependencies = [ "cprover_bindings", "serde", @@ -1169,7 +1169,7 @@ checksum = "a507befe795404456341dfab10cef66ead4c041f62b8b11bbb92bffe5d0953e0" [[package]] name = "std" -version = "0.29.0" +version = "0.30.0" dependencies = [ "kani", ] diff --git a/Cargo.toml b/Cargo.toml index 9e56e04c59ee..ea175207df0e 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-verifier" -version = "0.29.0" +version = "0.30.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 b2a4b0b68f60..dfcf9d616acf 100644 --- a/cprover_bindings/Cargo.toml +++ b/cprover_bindings/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "cprover_bindings" -version = "0.29.0" +version = "0.30.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml index ad335301e022..c47069f59d5d 100644 --- a/kani-compiler/Cargo.toml +++ b/kani-compiler/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-compiler" -version = "0.29.0" +version = "0.30.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml index f229d3300dc9..28bce4c30ce1 100644 --- a/kani-driver/Cargo.toml +++ b/kani-driver/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-driver" -version = "0.29.0" +version = "0.30.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 125397b2f4b0..a32dbb7b8db6 100644 --- a/kani_metadata/Cargo.toml +++ b/kani_metadata/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani_metadata" -version = "0.29.0" +version = "0.30.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/kani/Cargo.toml b/library/kani/Cargo.toml index 07dc445d0ac4..373ac53766e5 100644 --- a/library/kani/Cargo.toml +++ b/library/kani/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani" -version = "0.29.0" +version = "0.30.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 112ba4d5ca1e..0e2335f3c58b 100644 --- a/library/kani_macros/Cargo.toml +++ b/library/kani_macros/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani_macros" -version = "0.29.0" +version = "0.30.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/std/Cargo.toml b/library/std/Cargo.toml index 3dae3949d1ae..90a44ca50a7b 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.29.0" +version = "0.30.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 63b816b4fd4b..6feb881a93c7 100644 --- a/tools/build-kani/Cargo.toml +++ b/tools/build-kani/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "build-kani" -version = "0.29.0" +version = "0.30.0" edition = "2021" description = "Builds Kani, Sysroot and release bundle." license = "MIT OR Apache-2.0"