From 67cd1e6b074bfe91b8a4fde4c146a5ce6479276d Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Thu, 6 Mar 2025 11:45:00 -0600 Subject: [PATCH] Bump Kani version to 0.60.0 (#3923) ## What's Changed * Automatic cargo update to 2025-02-10 by @github-actions in https://github.com/model-checking/kani/pull/3880 * Bump tests/perf/s2n-quic from `82dd0b5` to `a5d8422` by @dependabot in https://github.com/model-checking/kani/pull/3882 * Fast fail feature - Stops verification process as soon as one failure is observed - Use case : CI speed up by @rajath-mk in https://github.com/model-checking/kani/pull/3879 * Autoharness Subcommand by @carolynzech in https://github.com/model-checking/kani/pull/3874 * Upgrade toolchain to 2/10 by @carolynzech in https://github.com/model-checking/kani/pull/3883 * Add loop-contracts doc to SUMMARY by @qinheping in https://github.com/model-checking/kani/pull/3886 * Support concrete playback for arrays of length 65 or greater by @carolynzech in https://github.com/model-checking/kani/pull/3888 * Automatic cargo update to 2025-02-17 by @github-actions in https://github.com/model-checking/kani/pull/3889 * Bump tests/perf/s2n-quic from `a5d8422` to `00e3371` by @dependabot in https://github.com/model-checking/kani/pull/3894 * Adjust PropertyClass of assertions to identify UB by @tautschnig in https://github.com/model-checking/kani/pull/3860 * Fix: regression test from #3888 has version control change by @carolynzech in https://github.com/model-checking/kani/pull/3892 * Upgrade toolchain to 2025-02-11 by @thanhnguyen-aws in https://github.com/model-checking/kani/pull/3887 * Remove isize overflow check for zst offsets by @carolynzech in https://github.com/model-checking/kani/pull/3897 * Automatic toolchain upgrade to nightly-2025-02-12 by @github-actions in https://github.com/model-checking/kani/pull/3898 * Upgrade the toolchain to 2025-02-21 by @zhassan-aws in https://github.com/model-checking/kani/pull/3899 * Automatic cargo update to 2025-02-24 by @github-actions in https://github.com/model-checking/kani/pull/3901 * Bump ncipollo/release-action from 1.15.0 to 1.16.0 by @dependabot in https://github.com/model-checking/kani/pull/3902 * Bump tests/perf/s2n-quic from `00e3371` to `cfb314b` by @dependabot in https://github.com/model-checking/kani/pull/3903 * Convert raw URL to link by @flba-eb in https://github.com/model-checking/kani/pull/3907 * Automatic cargo update to 2025-03-03 by @github-actions in https://github.com/model-checking/kani/pull/3913 * Install toolchain with rustup >= 1.28.0 by @tautschnig in https://github.com/model-checking/kani/pull/3917 * Bump tests/perf/s2n-quic from `cfb314b` to `d88faa4` by @dependabot in https://github.com/model-checking/kani/pull/3916 * Remove Ubuntu 20.04 CI usage by @tautschnig in https://github.com/model-checking/kani/pull/3918 * Move standard-library metrics script to verify-rust-std repo by @tautschnig in https://github.com/model-checking/kani/pull/3914 * scanner: Fix loop stats in overall function stats summary by @tautschnig in https://github.com/model-checking/kani/pull/3915 * Update toolchain to 2025-03-02 by @remi-delmas-3000 in https://github.com/model-checking/kani/pull/3911 ## New Contributors * @flba-eb made their first contribution in https://github.com/model-checking/kani/pull/3907 **Full Changelog**: https://github.com/model-checking/kani/compare/kani-0.59.0...kani-0.60.0 --------- Co-authored-by: Carolyn Zech --- CHANGELOG.md | 17 ++++++ Cargo.lock | 104 ++++++++++++++++----------------- 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_core/Cargo.toml | 2 +- library/kani_macros/Cargo.toml | 2 +- library/std/Cargo.toml | 2 +- tools/build-kani/Cargo.toml | 2 +- 12 files changed, 79 insertions(+), 62 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 7ae95fe7f52c..8c3f736e6a72 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -4,6 +4,23 @@ 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.60.0] + +### Breaking Changes +* Autoharness Subcommand by @carolynzech in https://github.com/model-checking/kani/pull/3874 +* Remove Ubuntu 20.04 CI usage by @tautschnig in https://github.com/model-checking/kani/pull/3918 + +### What's Changed +* Fast fail option - Stop verification process as soon as one failure is observed by @rajath-mk in https://github.com/model-checking/kani/pull/3879 +* Fail verification for UB regardless of whether `#[should_panic]` is enabled by @tautschnig in https://github.com/model-checking/kani/pull/3860 +* Support concrete playback for arrays of length 65 or greater by @carolynzech in https://github.com/model-checking/kani/pull/3888 +* Remove isize overflow check for zst offsets by @carolynzech in https://github.com/model-checking/kani/pull/3897 +* Support concrete playback for arrays of length 65 or greater by @carolynzech in https://github.com/model-checking/kani/pull/3888 +* Autoharness Misc. Improvements by @carolynzech in https://github.com/model-checking/kani/pull/3922 +* Update toolchain to 2025-03-02 by @remi-delmas-3000 @carolynzech @thanhnguyen-aws @zhassan-aws and @tautschnig + +**Full Changelog**: https://github.com/model-checking/kani/compare/kani-0.59.0...kani-0.60.0 + ## [0.59.0] ### Breaking Changes diff --git a/Cargo.lock b/Cargo.lock index 69990084ed31..258ee00c0568 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -101,9 +101,9 @@ dependencies = [ [[package]] name = "anyhow" -version = "1.0.96" +version = "1.0.97" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6b964d184e89d9b6b67dd2715bc8e74cf3107fb2b529990c90cf517326150bf4" +checksum = "dcfed56ad506cb2c684a14971b8861fdc3baaaae314b9e5f9bb532cbe3ba7a4f" [[package]] name = "arrayvec" @@ -176,7 +176,7 @@ dependencies = [ [[package]] name = "build-kani" -version = "0.59.0" +version = "0.60.0" dependencies = [ "anyhow", "cargo_metadata", @@ -192,9 +192,9 @@ checksum = "1fd0f2584146f6f2ef48085050886acf353beff7305ebd1ae69500e27c67f64b" [[package]] name = "bytes" -version = "1.10.0" +version = "1.10.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f61dac84819c6588b558454b194026eb1f09c293b9036ae9b159e74e73ab6cf9" +checksum = "d71b6127be86fdcfddb610f7182ac57211d4b18a3e9c82eb2d17662f2227ad6a" [[package]] name = "camino" @@ -225,7 +225,7 @@ dependencies = [ "semver", "serde", "serde_json", - "thiserror 2.0.11", + "thiserror 2.0.12", ] [[package]] @@ -397,7 +397,7 @@ dependencies = [ [[package]] name = "cprover_bindings" -version = "0.59.0" +version = "0.60.0" dependencies = [ "lazy_static", "linear-map", @@ -559,9 +559,9 @@ checksum = "fea41bba32d969b513997752735605054bc0dfa92b4c56bf1189f2e174be7a10" [[package]] name = "either" -version = "1.14.0" +version = "1.15.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b7914353092ddf589ad78f25c5c1c21b7f80b0ff8621e7c814c3485b5306da9d" +checksum = "48c757948c5ede0e46177b7add2e67155f70e33c07fea8284df6576da70b3719" [[package]] name = "encode_unicode" @@ -775,9 +775,9 @@ dependencies = [ [[package]] name = "indoc" -version = "2.0.5" +version = "2.0.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b248f5224d1d606005e02c97f5aa4e88eeb230488bcc03bc9ca4d7991399f2b5" +checksum = "f4c7245a08504955605670dbf141fceab975f15ca21570696aebe9d2e71576bd" [[package]] name = "is_terminal_polyfill" @@ -796,9 +796,9 @@ dependencies = [ [[package]] name = "itoa" -version = "1.0.14" +version = "1.0.15" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d75a2a4b1b190afb6f5425f10f6a8f959d2ea0b9c2b1d79553551850539e4674" +checksum = "4a5f13b858c8d314ee3e8f639011f7ccefe71f97f96e50151fb991f267928e2c" [[package]] name = "joinery" @@ -808,7 +808,7 @@ checksum = "72167d68f5fce3b8655487b8038691a3c9984ee769590f93f2a631f4ad64e4f5" [[package]] name = "kani" -version = "0.59.0" +version = "0.60.0" dependencies = [ "kani_core", "kani_macros", @@ -816,7 +816,7 @@ dependencies = [ [[package]] name = "kani-compiler" -version = "0.59.0" +version = "0.60.0" dependencies = [ "charon", "clap", @@ -855,7 +855,7 @@ dependencies = [ [[package]] name = "kani-driver" -version = "0.59.0" +version = "0.60.0" dependencies = [ "anyhow", "cargo_metadata", @@ -887,7 +887,7 @@ dependencies = [ [[package]] name = "kani-verifier" -version = "0.59.0" +version = "0.60.0" dependencies = [ "anyhow", "home", @@ -896,14 +896,14 @@ dependencies = [ [[package]] name = "kani_core" -version = "0.59.0" +version = "0.60.0" dependencies = [ "kani_macros", ] [[package]] name = "kani_macros" -version = "0.59.0" +version = "0.60.0" dependencies = [ "proc-macro-error2", "proc-macro2", @@ -913,7 +913,7 @@ dependencies = [ [[package]] name = "kani_metadata" -version = "0.59.0" +version = "0.60.0" dependencies = [ "clap", "cprover_bindings", @@ -1294,9 +1294,9 @@ dependencies = [ [[package]] name = "proc-macro2" -version = "1.0.93" +version = "1.0.94" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "60946a68e5f9d28b0dc1c21bb8a97ee7d018a8b322fa57838ba31cc878e22d99" +checksum = "a31971752e70b8b2686d7e46ec17fb38dad4051d94024c88df49b667caea9c84" dependencies = [ "unicode-ident", ] @@ -1312,9 +1312,9 @@ dependencies = [ [[package]] name = "quote" -version = "1.0.38" +version = "1.0.39" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0e4dccaaaf89514f546c693ddc140f729f958c247918a13380cccc6078391acc" +checksum = "c1f1914ce909e1658d9907913b4b91947430c7d9be598b15a1912935b8c04801" dependencies = [ "proc-macro2", ] @@ -1371,9 +1371,9 @@ dependencies = [ [[package]] name = "redox_syscall" -version = "0.5.9" +version = "0.5.10" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "82b568323e98e49e2a0899dcee453dd679fae22d69adf9b11dd508d1549b7e2f" +checksum = "0b8c0c260b63a8219631167be35e6a988e9554dbd323f8bd08439c8ed1302bd1" dependencies = [ "bitflags", ] @@ -1452,15 +1452,15 @@ dependencies = [ [[package]] name = "rustversion" -version = "1.0.19" +version = "1.0.20" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f7c45b9784283f1b2e7fb61b42047c2fd678ef0960d4f6f1eba131594cc369d4" +checksum = "eded382c5f5f786b989652c49544c4877d9f015cc22e145a5ea8ea66c2921cd2" [[package]] name = "ryu" -version = "1.0.19" +version = "1.0.20" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6ea1a2d0a644769cc99faa24c3ad26b379b786fe7c36fd3c546254801650e6dd" +checksum = "28d3b2b1366ec20994f1fd18c3c594f05c5dd4bc44d8bb0c1c632c8d6829481f" [[package]] name = "same-file" @@ -1491,9 +1491,9 @@ checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49" [[package]] name = "semver" -version = "1.0.25" +version = "1.0.26" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f79dfe2d285b0488816f30e700a7438c5a73d816b5b7d3ac72fbc48b0d185e03" +checksum = "56e6fa9c48d24d85fb3de5ad847117517440f6beceb7798af16b4a87d616b8d0" dependencies = [ "serde", ] @@ -1529,9 +1529,9 @@ dependencies = [ [[package]] name = "serde_json" -version = "1.0.139" +version = "1.0.140" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "44f86c3acccc9c65b153fe1b85a3be07fe5515274ec9f0653b4a0875731c72a6" +checksum = "20068b6e96dc6c9bd23e01df8827e6c7e1f2fddd43c21810382803c136b99373" dependencies = [ "indexmap", "itoa", @@ -1551,9 +1551,9 @@ dependencies = [ [[package]] name = "serde_stacker" -version = "0.1.11" +version = "0.1.12" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "babfccff5773ff80657f0ecf553c7c516bdc2eb16389c0918b36b73e7015276e" +checksum = "69c8defe6c780725cce4ec6ad3bd91e321baf6fa4e255df1f31e345d507ef01a" dependencies = [ "serde", "stacker", @@ -1632,7 +1632,7 @@ dependencies = [ [[package]] name = "std" -version = "0.59.0" +version = "0.60.0" dependencies = [ "kani", ] @@ -1680,9 +1680,9 @@ dependencies = [ [[package]] name = "syn" -version = "2.0.98" +version = "2.0.99" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "36147f1a48ae0ec2b5b3bc5b537d267457555a10dc06f3dbc8cb11ba3006d3b1" +checksum = "e02e925281e18ffd9d640e234264753c43edc62d64b2d4cf898f1bc5e75f3fc2" dependencies = [ "proc-macro2", "quote", @@ -1726,11 +1726,11 @@ dependencies = [ [[package]] name = "thiserror" -version = "2.0.11" +version = "2.0.12" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d452f284b73e6d76dd36758a0c8684b1d5be31f92b89d07fd5822175732206fc" +checksum = "567b8a2dae586314f7be2a752ec7474332959c6460e02bde30d702a66d488708" dependencies = [ - "thiserror-impl 2.0.11", + "thiserror-impl 2.0.12", ] [[package]] @@ -1746,9 +1746,9 @@ dependencies = [ [[package]] name = "thiserror-impl" -version = "2.0.11" +version = "2.0.12" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "26afc1baea8a989337eeb52b6e72a039780ce45c3edfcc9c5b9d112feeb173c2" +checksum = "7f7cf42b4507d8ea322120659672cf1b9dbb93f8f2d4ecfd6e51350ff5b17a1d" dependencies = [ "proc-macro2", "quote", @@ -1767,9 +1767,9 @@ dependencies = [ [[package]] name = "time" -version = "0.3.37" +version = "0.3.38" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "35e7868883861bd0e56d9ac6efcaaca0d6d5d82a2a7ec8209ff492c07cf37b21" +checksum = "bb041120f25f8fbe8fd2dbe4671c7c2ed74d83be2e7a77529bf7e0790ae3f472" dependencies = [ "deranged", "itoa", @@ -1784,15 +1784,15 @@ dependencies = [ [[package]] name = "time-core" -version = "0.1.2" +version = "0.1.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ef927ca75afb808a4d64dd374f00a2adf8d0fcff8e7b184af886c3c87ec4a3f3" +checksum = "765c97a5b985b7c11d7bc27fa927dc4fe6af3a6dfb021d28deb60d3bf51e76ef" [[package]] name = "time-macros" -version = "0.2.19" +version = "0.2.20" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2834e6017e3e5e4b9834939793b282bc03b37a3336245fa820e35e233e2a85de" +checksum = "e8093bc3e81c3bc5f7879de09619d06c9a5a5e45ca44dfeeb7225bae38005c5c" dependencies = [ "num-conv", "time-core", @@ -1986,9 +1986,9 @@ dependencies = [ [[package]] name = "unicode-ident" -version = "1.0.17" +version = "1.0.18" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "00e2473a93778eb0bad35909dff6a10d28e63f792f16ed15e404fca9d5eeedbe" +checksum = "5a5f39404a5da50712a4c1eecf25e90dd62b613502b7e925fd4e4d19b5c96512" [[package]] name = "unicode-segmentation" diff --git a/Cargo.toml b/Cargo.toml index 4948246d5110..beabf68f6e53 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-verifier" -version = "0.59.0" +version = "0.60.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 b35626e3d5f4..8c8cf77fd411 100644 --- a/cprover_bindings/Cargo.toml +++ b/cprover_bindings/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "cprover_bindings" -version = "0.59.0" +version = "0.60.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml index e2636f5fcd64..f11932a7387e 100644 --- a/kani-compiler/Cargo.toml +++ b/kani-compiler/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-compiler" -version = "0.59.0" +version = "0.60.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml index ec39fbf67dec..e6efa9460afb 100644 --- a/kani-driver/Cargo.toml +++ b/kani-driver/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-driver" -version = "0.59.0" +version = "0.60.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 b4db86ebed1e..038b9e235663 100644 --- a/kani_metadata/Cargo.toml +++ b/kani_metadata/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani_metadata" -version = "0.59.0" +version = "0.60.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/kani/Cargo.toml b/library/kani/Cargo.toml index d559be65a88f..4b32b92485e8 100644 --- a/library/kani/Cargo.toml +++ b/library/kani/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani" -version = "0.59.0" +version = "0.60.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/kani_core/Cargo.toml b/library/kani_core/Cargo.toml index b474e15d7d0c..17338d03f12f 100644 --- a/library/kani_core/Cargo.toml +++ b/library/kani_core/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani_core" -version = "0.59.0" +version = "0.60.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 85e3ee2ed48c..8a68cd8cc124 100644 --- a/library/kani_macros/Cargo.toml +++ b/library/kani_macros/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani_macros" -version = "0.59.0" +version = "0.60.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/std/Cargo.toml b/library/std/Cargo.toml index 223310d52726..b4ca6fee7822 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.59.0" +version = "0.60.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 8d837a9b0e3f..23632adc48ec 100644 --- a/tools/build-kani/Cargo.toml +++ b/tools/build-kani/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "build-kani" -version = "0.59.0" +version = "0.60.0" edition = "2021" description = "Builds Kani, Sysroot and release bundle." license = "MIT OR Apache-2.0"