Skip to content

Commit 67cd1e6

Browse files
Bump Kani version to 0.60.0 (#3923)
## What's Changed * Automatic cargo update to 2025-02-10 by @github-actions in #3880 * Bump tests/perf/s2n-quic from `82dd0b5` to `a5d8422` by @dependabot in #3882 * Fast fail feature - Stops verification process as soon as one failure is observed - Use case : CI speed up by @rajath-mk in #3879 * Autoharness Subcommand by @carolynzech in #3874 * Upgrade toolchain to 2/10 by @carolynzech in #3883 * Add loop-contracts doc to SUMMARY by @qinheping in #3886 * Support concrete playback for arrays of length 65 or greater by @carolynzech in #3888 * Automatic cargo update to 2025-02-17 by @github-actions in #3889 * Bump tests/perf/s2n-quic from `a5d8422` to `00e3371` by @dependabot in #3894 * Adjust PropertyClass of assertions to identify UB by @tautschnig in #3860 * Fix: regression test from #3888 has version control change by @carolynzech in #3892 * Upgrade toolchain to 2025-02-11 by @thanhnguyen-aws in #3887 * Remove isize overflow check for zst offsets by @carolynzech in #3897 * Automatic toolchain upgrade to nightly-2025-02-12 by @github-actions in #3898 * Upgrade the toolchain to 2025-02-21 by @zhassan-aws in #3899 * Automatic cargo update to 2025-02-24 by @github-actions in #3901 * Bump ncipollo/release-action from 1.15.0 to 1.16.0 by @dependabot in #3902 * Bump tests/perf/s2n-quic from `00e3371` to `cfb314b` by @dependabot in #3903 * Convert raw URL to link by @flba-eb in #3907 * Automatic cargo update to 2025-03-03 by @github-actions in #3913 * Install toolchain with rustup >= 1.28.0 by @tautschnig in #3917 * Bump tests/perf/s2n-quic from `cfb314b` to `d88faa4` by @dependabot in #3916 * Remove Ubuntu 20.04 CI usage by @tautschnig in #3918 * Move standard-library metrics script to verify-rust-std repo by @tautschnig in #3914 * scanner: Fix loop stats in overall function stats summary by @tautschnig in #3915 * Update toolchain to 2025-03-02 by @remi-delmas-3000 in #3911 ## New Contributors * @flba-eb made their first contribution in #3907 **Full Changelog**: kani-0.59.0...kani-0.60.0 --------- Co-authored-by: Carolyn Zech <cmzech@amazon.com>
1 parent 68cb4ee commit 67cd1e6

File tree

12 files changed

+79
-62
lines changed

12 files changed

+79
-62
lines changed

CHANGELOG.md

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,23 @@ This file contains notable changes (e.g. breaking changes, major changes, etc.)
44

55
This file was introduced starting Kani 0.23.0, so it only contains changes from version 0.23.0 onwards.
66

7+
## [0.60.0]
8+
9+
### Breaking Changes
10+
* Autoharness Subcommand by @carolynzech in https://github.com/model-checking/kani/pull/3874
11+
* Remove Ubuntu 20.04 CI usage by @tautschnig in https://github.com/model-checking/kani/pull/3918
12+
13+
### What's Changed
14+
* 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
15+
* Fail verification for UB regardless of whether `#[should_panic]` is enabled by @tautschnig in https://github.com/model-checking/kani/pull/3860
16+
* Support concrete playback for arrays of length 65 or greater by @carolynzech in https://github.com/model-checking/kani/pull/3888
17+
* Remove isize overflow check for zst offsets by @carolynzech in https://github.com/model-checking/kani/pull/3897
18+
* Support concrete playback for arrays of length 65 or greater by @carolynzech in https://github.com/model-checking/kani/pull/3888
19+
* Autoharness Misc. Improvements by @carolynzech in https://github.com/model-checking/kani/pull/3922
20+
* Update toolchain to 2025-03-02 by @remi-delmas-3000 @carolynzech @thanhnguyen-aws @zhassan-aws and @tautschnig
21+
22+
**Full Changelog**: https://github.com/model-checking/kani/compare/kani-0.59.0...kani-0.60.0
23+
724
## [0.59.0]
825

926
### Breaking Changes

Cargo.lock

Lines changed: 52 additions & 52 deletions
Original file line numberDiff line numberDiff line change
@@ -101,9 +101,9 @@ dependencies = [
101101

102102
[[package]]
103103
name = "anyhow"
104-
version = "1.0.96"
104+
version = "1.0.97"
105105
source = "registry+https://github.com/rust-lang/crates.io-index"
106-
checksum = "6b964d184e89d9b6b67dd2715bc8e74cf3107fb2b529990c90cf517326150bf4"
106+
checksum = "dcfed56ad506cb2c684a14971b8861fdc3baaaae314b9e5f9bb532cbe3ba7a4f"
107107

108108
[[package]]
109109
name = "arrayvec"
@@ -176,7 +176,7 @@ dependencies = [
176176

177177
[[package]]
178178
name = "build-kani"
179-
version = "0.59.0"
179+
version = "0.60.0"
180180
dependencies = [
181181
"anyhow",
182182
"cargo_metadata",
@@ -192,9 +192,9 @@ checksum = "1fd0f2584146f6f2ef48085050886acf353beff7305ebd1ae69500e27c67f64b"
192192

193193
[[package]]
194194
name = "bytes"
195-
version = "1.10.0"
195+
version = "1.10.1"
196196
source = "registry+https://github.com/rust-lang/crates.io-index"
197-
checksum = "f61dac84819c6588b558454b194026eb1f09c293b9036ae9b159e74e73ab6cf9"
197+
checksum = "d71b6127be86fdcfddb610f7182ac57211d4b18a3e9c82eb2d17662f2227ad6a"
198198

199199
[[package]]
200200
name = "camino"
@@ -225,7 +225,7 @@ dependencies = [
225225
"semver",
226226
"serde",
227227
"serde_json",
228-
"thiserror 2.0.11",
228+
"thiserror 2.0.12",
229229
]
230230

231231
[[package]]
@@ -397,7 +397,7 @@ dependencies = [
397397

398398
[[package]]
399399
name = "cprover_bindings"
400-
version = "0.59.0"
400+
version = "0.60.0"
401401
dependencies = [
402402
"lazy_static",
403403
"linear-map",
@@ -559,9 +559,9 @@ checksum = "fea41bba32d969b513997752735605054bc0dfa92b4c56bf1189f2e174be7a10"
559559

560560
[[package]]
561561
name = "either"
562-
version = "1.14.0"
562+
version = "1.15.0"
563563
source = "registry+https://github.com/rust-lang/crates.io-index"
564-
checksum = "b7914353092ddf589ad78f25c5c1c21b7f80b0ff8621e7c814c3485b5306da9d"
564+
checksum = "48c757948c5ede0e46177b7add2e67155f70e33c07fea8284df6576da70b3719"
565565

566566
[[package]]
567567
name = "encode_unicode"
@@ -775,9 +775,9 @@ dependencies = [
775775

776776
[[package]]
777777
name = "indoc"
778-
version = "2.0.5"
778+
version = "2.0.6"
779779
source = "registry+https://github.com/rust-lang/crates.io-index"
780-
checksum = "b248f5224d1d606005e02c97f5aa4e88eeb230488bcc03bc9ca4d7991399f2b5"
780+
checksum = "f4c7245a08504955605670dbf141fceab975f15ca21570696aebe9d2e71576bd"
781781

782782
[[package]]
783783
name = "is_terminal_polyfill"
@@ -796,9 +796,9 @@ dependencies = [
796796

797797
[[package]]
798798
name = "itoa"
799-
version = "1.0.14"
799+
version = "1.0.15"
800800
source = "registry+https://github.com/rust-lang/crates.io-index"
801-
checksum = "d75a2a4b1b190afb6f5425f10f6a8f959d2ea0b9c2b1d79553551850539e4674"
801+
checksum = "4a5f13b858c8d314ee3e8f639011f7ccefe71f97f96e50151fb991f267928e2c"
802802

803803
[[package]]
804804
name = "joinery"
@@ -808,15 +808,15 @@ checksum = "72167d68f5fce3b8655487b8038691a3c9984ee769590f93f2a631f4ad64e4f5"
808808

809809
[[package]]
810810
name = "kani"
811-
version = "0.59.0"
811+
version = "0.60.0"
812812
dependencies = [
813813
"kani_core",
814814
"kani_macros",
815815
]
816816

817817
[[package]]
818818
name = "kani-compiler"
819-
version = "0.59.0"
819+
version = "0.60.0"
820820
dependencies = [
821821
"charon",
822822
"clap",
@@ -855,7 +855,7 @@ dependencies = [
855855

856856
[[package]]
857857
name = "kani-driver"
858-
version = "0.59.0"
858+
version = "0.60.0"
859859
dependencies = [
860860
"anyhow",
861861
"cargo_metadata",
@@ -887,7 +887,7 @@ dependencies = [
887887

888888
[[package]]
889889
name = "kani-verifier"
890-
version = "0.59.0"
890+
version = "0.60.0"
891891
dependencies = [
892892
"anyhow",
893893
"home",
@@ -896,14 +896,14 @@ dependencies = [
896896

897897
[[package]]
898898
name = "kani_core"
899-
version = "0.59.0"
899+
version = "0.60.0"
900900
dependencies = [
901901
"kani_macros",
902902
]
903903

904904
[[package]]
905905
name = "kani_macros"
906-
version = "0.59.0"
906+
version = "0.60.0"
907907
dependencies = [
908908
"proc-macro-error2",
909909
"proc-macro2",
@@ -913,7 +913,7 @@ dependencies = [
913913

914914
[[package]]
915915
name = "kani_metadata"
916-
version = "0.59.0"
916+
version = "0.60.0"
917917
dependencies = [
918918
"clap",
919919
"cprover_bindings",
@@ -1294,9 +1294,9 @@ dependencies = [
12941294

12951295
[[package]]
12961296
name = "proc-macro2"
1297-
version = "1.0.93"
1297+
version = "1.0.94"
12981298
source = "registry+https://github.com/rust-lang/crates.io-index"
1299-
checksum = "60946a68e5f9d28b0dc1c21bb8a97ee7d018a8b322fa57838ba31cc878e22d99"
1299+
checksum = "a31971752e70b8b2686d7e46ec17fb38dad4051d94024c88df49b667caea9c84"
13001300
dependencies = [
13011301
"unicode-ident",
13021302
]
@@ -1312,9 +1312,9 @@ dependencies = [
13121312

13131313
[[package]]
13141314
name = "quote"
1315-
version = "1.0.38"
1315+
version = "1.0.39"
13161316
source = "registry+https://github.com/rust-lang/crates.io-index"
1317-
checksum = "0e4dccaaaf89514f546c693ddc140f729f958c247918a13380cccc6078391acc"
1317+
checksum = "c1f1914ce909e1658d9907913b4b91947430c7d9be598b15a1912935b8c04801"
13181318
dependencies = [
13191319
"proc-macro2",
13201320
]
@@ -1371,9 +1371,9 @@ dependencies = [
13711371

13721372
[[package]]
13731373
name = "redox_syscall"
1374-
version = "0.5.9"
1374+
version = "0.5.10"
13751375
source = "registry+https://github.com/rust-lang/crates.io-index"
1376-
checksum = "82b568323e98e49e2a0899dcee453dd679fae22d69adf9b11dd508d1549b7e2f"
1376+
checksum = "0b8c0c260b63a8219631167be35e6a988e9554dbd323f8bd08439c8ed1302bd1"
13771377
dependencies = [
13781378
"bitflags",
13791379
]
@@ -1452,15 +1452,15 @@ dependencies = [
14521452

14531453
[[package]]
14541454
name = "rustversion"
1455-
version = "1.0.19"
1455+
version = "1.0.20"
14561456
source = "registry+https://github.com/rust-lang/crates.io-index"
1457-
checksum = "f7c45b9784283f1b2e7fb61b42047c2fd678ef0960d4f6f1eba131594cc369d4"
1457+
checksum = "eded382c5f5f786b989652c49544c4877d9f015cc22e145a5ea8ea66c2921cd2"
14581458

14591459
[[package]]
14601460
name = "ryu"
1461-
version = "1.0.19"
1461+
version = "1.0.20"
14621462
source = "registry+https://github.com/rust-lang/crates.io-index"
1463-
checksum = "6ea1a2d0a644769cc99faa24c3ad26b379b786fe7c36fd3c546254801650e6dd"
1463+
checksum = "28d3b2b1366ec20994f1fd18c3c594f05c5dd4bc44d8bb0c1c632c8d6829481f"
14641464

14651465
[[package]]
14661466
name = "same-file"
@@ -1491,9 +1491,9 @@ checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49"
14911491

14921492
[[package]]
14931493
name = "semver"
1494-
version = "1.0.25"
1494+
version = "1.0.26"
14951495
source = "registry+https://github.com/rust-lang/crates.io-index"
1496-
checksum = "f79dfe2d285b0488816f30e700a7438c5a73d816b5b7d3ac72fbc48b0d185e03"
1496+
checksum = "56e6fa9c48d24d85fb3de5ad847117517440f6beceb7798af16b4a87d616b8d0"
14971497
dependencies = [
14981498
"serde",
14991499
]
@@ -1529,9 +1529,9 @@ dependencies = [
15291529

15301530
[[package]]
15311531
name = "serde_json"
1532-
version = "1.0.139"
1532+
version = "1.0.140"
15331533
source = "registry+https://github.com/rust-lang/crates.io-index"
1534-
checksum = "44f86c3acccc9c65b153fe1b85a3be07fe5515274ec9f0653b4a0875731c72a6"
1534+
checksum = "20068b6e96dc6c9bd23e01df8827e6c7e1f2fddd43c21810382803c136b99373"
15351535
dependencies = [
15361536
"indexmap",
15371537
"itoa",
@@ -1551,9 +1551,9 @@ dependencies = [
15511551

15521552
[[package]]
15531553
name = "serde_stacker"
1554-
version = "0.1.11"
1554+
version = "0.1.12"
15551555
source = "registry+https://github.com/rust-lang/crates.io-index"
1556-
checksum = "babfccff5773ff80657f0ecf553c7c516bdc2eb16389c0918b36b73e7015276e"
1556+
checksum = "69c8defe6c780725cce4ec6ad3bd91e321baf6fa4e255df1f31e345d507ef01a"
15571557
dependencies = [
15581558
"serde",
15591559
"stacker",
@@ -1632,7 +1632,7 @@ dependencies = [
16321632

16331633
[[package]]
16341634
name = "std"
1635-
version = "0.59.0"
1635+
version = "0.60.0"
16361636
dependencies = [
16371637
"kani",
16381638
]
@@ -1680,9 +1680,9 @@ dependencies = [
16801680

16811681
[[package]]
16821682
name = "syn"
1683-
version = "2.0.98"
1683+
version = "2.0.99"
16841684
source = "registry+https://github.com/rust-lang/crates.io-index"
1685-
checksum = "36147f1a48ae0ec2b5b3bc5b537d267457555a10dc06f3dbc8cb11ba3006d3b1"
1685+
checksum = "e02e925281e18ffd9d640e234264753c43edc62d64b2d4cf898f1bc5e75f3fc2"
16861686
dependencies = [
16871687
"proc-macro2",
16881688
"quote",
@@ -1726,11 +1726,11 @@ dependencies = [
17261726

17271727
[[package]]
17281728
name = "thiserror"
1729-
version = "2.0.11"
1729+
version = "2.0.12"
17301730
source = "registry+https://github.com/rust-lang/crates.io-index"
1731-
checksum = "d452f284b73e6d76dd36758a0c8684b1d5be31f92b89d07fd5822175732206fc"
1731+
checksum = "567b8a2dae586314f7be2a752ec7474332959c6460e02bde30d702a66d488708"
17321732
dependencies = [
1733-
"thiserror-impl 2.0.11",
1733+
"thiserror-impl 2.0.12",
17341734
]
17351735

17361736
[[package]]
@@ -1746,9 +1746,9 @@ dependencies = [
17461746

17471747
[[package]]
17481748
name = "thiserror-impl"
1749-
version = "2.0.11"
1749+
version = "2.0.12"
17501750
source = "registry+https://github.com/rust-lang/crates.io-index"
1751-
checksum = "26afc1baea8a989337eeb52b6e72a039780ce45c3edfcc9c5b9d112feeb173c2"
1751+
checksum = "7f7cf42b4507d8ea322120659672cf1b9dbb93f8f2d4ecfd6e51350ff5b17a1d"
17521752
dependencies = [
17531753
"proc-macro2",
17541754
"quote",
@@ -1767,9 +1767,9 @@ dependencies = [
17671767

17681768
[[package]]
17691769
name = "time"
1770-
version = "0.3.37"
1770+
version = "0.3.38"
17711771
source = "registry+https://github.com/rust-lang/crates.io-index"
1772-
checksum = "35e7868883861bd0e56d9ac6efcaaca0d6d5d82a2a7ec8209ff492c07cf37b21"
1772+
checksum = "bb041120f25f8fbe8fd2dbe4671c7c2ed74d83be2e7a77529bf7e0790ae3f472"
17731773
dependencies = [
17741774
"deranged",
17751775
"itoa",
@@ -1784,15 +1784,15 @@ dependencies = [
17841784

17851785
[[package]]
17861786
name = "time-core"
1787-
version = "0.1.2"
1787+
version = "0.1.3"
17881788
source = "registry+https://github.com/rust-lang/crates.io-index"
1789-
checksum = "ef927ca75afb808a4d64dd374f00a2adf8d0fcff8e7b184af886c3c87ec4a3f3"
1789+
checksum = "765c97a5b985b7c11d7bc27fa927dc4fe6af3a6dfb021d28deb60d3bf51e76ef"
17901790

17911791
[[package]]
17921792
name = "time-macros"
1793-
version = "0.2.19"
1793+
version = "0.2.20"
17941794
source = "registry+https://github.com/rust-lang/crates.io-index"
1795-
checksum = "2834e6017e3e5e4b9834939793b282bc03b37a3336245fa820e35e233e2a85de"
1795+
checksum = "e8093bc3e81c3bc5f7879de09619d06c9a5a5e45ca44dfeeb7225bae38005c5c"
17961796
dependencies = [
17971797
"num-conv",
17981798
"time-core",
@@ -1986,9 +1986,9 @@ dependencies = [
19861986

19871987
[[package]]
19881988
name = "unicode-ident"
1989-
version = "1.0.17"
1989+
version = "1.0.18"
19901990
source = "registry+https://github.com/rust-lang/crates.io-index"
1991-
checksum = "00e2473a93778eb0bad35909dff6a10d28e63f792f16ed15e404fca9d5eeedbe"
1991+
checksum = "5a5f39404a5da50712a4c1eecf25e90dd62b613502b7e925fd4e4d19b5c96512"
19921992

19931993
[[package]]
19941994
name = "unicode-segmentation"

Cargo.toml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33

44
[package]
55
name = "kani-verifier"
6-
version = "0.59.0"
6+
version = "0.60.0"
77
edition = "2021"
88
description = "A bit-precise model checker for Rust."
99
readme = "README.md"

cprover_bindings/Cargo.toml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33

44
[package]
55
name = "cprover_bindings"
6-
version = "0.59.0"
6+
version = "0.60.0"
77
edition = "2021"
88
license = "MIT OR Apache-2.0"
99
publish = false

kani-compiler/Cargo.toml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33

44
[package]
55
name = "kani-compiler"
6-
version = "0.59.0"
6+
version = "0.60.0"
77
edition = "2021"
88
license = "MIT OR Apache-2.0"
99
publish = false

kani-driver/Cargo.toml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33

44
[package]
55
name = "kani-driver"
6-
version = "0.59.0"
6+
version = "0.60.0"
77
edition = "2021"
88
description = "Build a project with Kani and run all proof harnesses"
99
license = "MIT OR Apache-2.0"

0 commit comments

Comments
 (0)