From 6d9575e049fca615c7f4b20edebbeee05331c5e5 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 5 Oct 2023 12:25:57 +0200 Subject: [PATCH] Bump Kani version to 0.38.0 (#2798) Next Kani release. Also includes fixes to changelog formatting. --- CHANGELOG.md | 34 ++++++++++++++++++++++++++-------- 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, 44 insertions(+), 26 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 7b987e5a8f76..760748037be5 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -4,6 +4,24 @@ 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.38.0] + +### Major Changes + +* Deprecate `any_slice` by @zhassan-aws in https://github.com/model-checking/kani/pull/2789 + +### What's Changed + +* Provide better error message for invalid stubs by @JustusAdam in https://github.com/model-checking/kani/pull/2787 +* Simple Stubbing with Contracts by @JustusAdam in https://github.com/model-checking/kani/pull/2746 +* Avoid mismatch when generating structs that represent scalar data but also include ZSTs by @adpaco-aws in https://github.com/model-checking/kani/pull/2794 +* Prevent kani crash during setup for first time by @jaisnan in https://github.com/model-checking/kani/pull/2799 +* Create concrete playback temp files in source directory by @tautschnig in https://github.com/model-checking/kani/pull/2804 +* Bump CBMC version by @zhassan-aws in https://github.com/model-checking/kani/pull/2796 +* Update Rust toolchain to 2023-09-23 by @tautschnig in https://github.com/model-checking/kani/pull/2806 + +**Full Changelog**: https://github.com/model-checking/kani/compare/kani-0.37.0...kani-0.38.0 + ## [0.37.0] ### Major Changes @@ -11,7 +29,7 @@ This file was introduced starting Kani 0.23.0, so it only contains changes from * Delete obsolete stubs for `Vec` and related options by @zhassan-aws in https://github.com/model-checking/kani/pull/2770 * Add support for the ARM64 Linux platform by @adpaco-aws in https://github.com/model-checking/kani/pull/2757 -## What's Changed +### What's Changed * Function Contracts: Support for defining and checking `requires` and `ensures` clauses by @JustusAdam in https://github.com/model-checking/kani/pull/2655 * Force `any_vec` capacity to match length by @celinval in https://github.com/model-checking/kani/pull/2765 @@ -24,7 +42,7 @@ This file was introduced starting Kani 0.23.0, so it only contains changes from ## [0.36.0] -## What's Changed +### What's Changed * Enable `-Z stubbing` and error out instead of ignoring stub by @celinval in https://github.com/model-checking/kani/pull/2678 * Enable concrete playback for failure of UB checks by @zhassan-aws in https://github.com/model-checking/kani/pull/2727 @@ -35,7 +53,7 @@ This file was introduced starting Kani 0.23.0, so it only contains changes from ## [0.35.0] -## What's Changed +### What's Changed * Add support to `simd_bitmask` by @celinval in https://github.com/model-checking/kani/pull/2677 * Add integer overflow checking for `simd_div` and `simd_rem` by @reisnera in https://github.com/model-checking/kani/pull/2645 @@ -52,7 +70,7 @@ By default, Kani will now run CBMC with CaDiCaL, since this solver has outperfor User's should still be able to select Minisat (or a different solver) either by using `#[solver]` harness attribute, or by passing `--solver=` command line option. -## What's Changed +### What's Changed * Allow specifying the scheduling strategy in #[kani_proof] for async functions by @fzaiser in https://github.com/model-checking/kani/pull/1661 * Support for stubbing out foreign functions by @feliperodri in https://github.com/model-checking/kani/pull/2658 @@ -67,7 +85,7 @@ or by passing `--solver=` command line option. ## [0.33.0] -## What's Changed +### What's Changed * Add support for sysconf by @feliperodri in https://github.com/model-checking/kani/pull/2557 * Print Kani version by @adpaco-aws in https://github.com/model-checking/kani/pull/2619 * Upgrade Rust toolchain to nightly-2023-07-01 by @qinheping in https://github.com/model-checking/kani/pull/2616 @@ -77,7 +95,7 @@ or by passing `--solver=` command line option. ## [0.32.0] -## What's Changed +### What's Changed * Add kani::spawn and an executor to the Kani library by @fzaiser in https://github.com/model-checking/kani/pull/1659 * Add "kani" configuration key to enable conditional compilation in build scripts by @celinval in https://github.com/model-checking/kani/pull/2297 @@ -91,7 +109,7 @@ or by passing `--solver=` command line option. ## [0.31.0] -## What's Changed +### What's Changed * Add `--exact` flag by @jaisnan in https://github.com/model-checking/kani/pull/2527 * Build the verification libraries using Kani compiler by @celinval in https://github.com/model-checking/kani/pull/2534 * Verify all Kani attributes in all crate items upfront by @celinval in https://github.com/model-checking/kani/pull/2536 @@ -102,7 +120,7 @@ or by passing `--solver=` command line option. ## [0.30.0] -## What's Changed +### 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 diff --git a/Cargo.lock b/Cargo.lock index 59770bbda6d2..5aad3f1d4614 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -119,7 +119,7 @@ dependencies = [ [[package]] name = "build-kani" -version = "0.37.0" +version = "0.38.0" dependencies = [ "anyhow", "cargo_metadata", @@ -264,7 +264,7 @@ dependencies = [ [[package]] name = "cprover_bindings" -version = "0.37.0" +version = "0.38.0" dependencies = [ "lazy_static", "linear-map", @@ -463,14 +463,14 @@ checksum = "af150ab688ff2122fcef229be89cb50dd66af9e01a4ff320cc137eecc9bacc38" [[package]] name = "kani" -version = "0.37.0" +version = "0.38.0" dependencies = [ "kani_macros", ] [[package]] name = "kani-compiler" -version = "0.37.0" +version = "0.38.0" dependencies = [ "clap", "cprover_bindings", @@ -491,7 +491,7 @@ dependencies = [ [[package]] name = "kani-driver" -version = "0.37.0" +version = "0.38.0" dependencies = [ "anyhow", "cargo_metadata", @@ -519,7 +519,7 @@ dependencies = [ [[package]] name = "kani-verifier" -version = "0.37.0" +version = "0.38.0" dependencies = [ "anyhow", "home", @@ -528,7 +528,7 @@ dependencies = [ [[package]] name = "kani_macros" -version = "0.37.0" +version = "0.38.0" dependencies = [ "proc-macro-error", "proc-macro2", @@ -538,7 +538,7 @@ dependencies = [ [[package]] name = "kani_metadata" -version = "0.37.0" +version = "0.38.0" dependencies = [ "clap", "cprover_bindings", @@ -1115,7 +1115,7 @@ checksum = "942b4a808e05215192e39f4ab80813e599068285906cc91aa64f923db842bd5a" [[package]] name = "std" -version = "0.37.0" +version = "0.38.0" dependencies = [ "kani", ] diff --git a/Cargo.toml b/Cargo.toml index d99a2ffde289..e2a61bdd95b3 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-verifier" -version = "0.37.0" +version = "0.38.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 e8c523ad4bd3..2a1d5e50c0ac 100644 --- a/cprover_bindings/Cargo.toml +++ b/cprover_bindings/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "cprover_bindings" -version = "0.37.0" +version = "0.38.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml index c888afac5f01..f0758cd28ecf 100644 --- a/kani-compiler/Cargo.toml +++ b/kani-compiler/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-compiler" -version = "0.37.0" +version = "0.38.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml index 2f01fa9e83dd..3238e9bc599c 100644 --- a/kani-driver/Cargo.toml +++ b/kani-driver/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-driver" -version = "0.37.0" +version = "0.38.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 0deb1b994821..c9fb64016b7c 100644 --- a/kani_metadata/Cargo.toml +++ b/kani_metadata/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani_metadata" -version = "0.37.0" +version = "0.38.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/kani/Cargo.toml b/library/kani/Cargo.toml index 97e30ba6294e..358e1a3c20d8 100644 --- a/library/kani/Cargo.toml +++ b/library/kani/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani" -version = "0.37.0" +version = "0.38.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 42c30f20c29a..535dd19a2a03 100644 --- a/library/kani_macros/Cargo.toml +++ b/library/kani_macros/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani_macros" -version = "0.37.0" +version = "0.38.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/std/Cargo.toml b/library/std/Cargo.toml index 2a5ed385c8dc..157ef0acc613 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.37.0" +version = "0.38.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 014f2949af0f..bfd81c1be85e 100644 --- a/tools/build-kani/Cargo.toml +++ b/tools/build-kani/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "build-kani" -version = "0.37.0" +version = "0.38.0" edition = "2021" description = "Builds Kani, Sysroot and release bundle." license = "MIT OR Apache-2.0"