Skip to content

Commit 96f7e59

Browse files
authored
Bump Kani version to 0.64.0 (#4198)
Auto generated release notes: ## What's Changed * Edit quantifiers' documentation. by @thanhnguyen-aws in #4142 * Fix the bug of using multiple hidden variables for the prev of the same Expr by @thanhnguyen-aws in #4150 * Remove `assess` subcommand by @carolynzech in #4111 * Optimize goto binary exporting in `cprover_bindings` by @AlexanderPortland in #4148 * Add the option to generate performance flamegraphs by @AlexanderPortland in #4138 * Fix the bug: Static union values can panic Kani by @thanhnguyen-aws in #4112 * Update toolchain to 2025-06-13 by @carolynzech in #4152 * Automatic cargo update to 2025-06-16 by @github-actions in #4156 * Major-version update cargo dependencies by @tautschnig in #4158 * Upgrade Rust toolchain to 2025-06-16 by @tautschnig in #4157 * Bump tests/perf/s2n-quic from `3129ad5` to `c6e694e` by @dependabot in #4160 * Bump tests/perf/s2n-quic from `c6e694e` to `b1b5bf8` by @dependabot in #4164 * Upgrade Rust toolchain to 2025-06-17 by @tautschnig in #4163 * Automatic cargo update to 2025-06-23 by @github-actions in #4172 * Stub panics during MIR transformation by @AlexanderPortland in #4169 * Bump tests/perf/s2n-quic from `b1b5bf8` to `32ba87d` by @dependabot in #4175 * Handle enums with zero or one variants by @zhassan-aws in #4171 * Introduce compiler timing script & CI job by @AlexanderPortland in #4154 * Upgrade Rust toolchain to 2025-06-18 by @tautschnig in #4166 * Cache dependencies for CI jobs by @AlexanderPortland in #4181 * Autoharness: Derive `Arbitrary` for structs and enums by @carolynzech in #4167 * Upgrade Rust toolchain to 2025-06-27 by @tautschnig in #4182 * Include wget in dependencies by @zhassan-aws in #4183 * Automatic cargo update to 2025-06-30 by @github-actions in #4186 * Add support for loop assigns in loop contracts by @thanhnguyen-aws in #4174 * Upgrade toolchain to 06/30 by @carolynzech in #4188 * Optimize reachability with non-mutating global passes by @AlexanderPortland in #4177 * Bump tests/perf/s2n-quic from `32ba87d` to `b8f8cca` by @dependabot in #4190 * Bump ncipollo/release-action from 1.16.0 to 1.18.0 by @dependabot in #4191 * Upgrade toolchain to 07/02 by @carolynzech in #4195 * Automatic Derivation Fixes by @carolynzech in #4194 **Full Changelog**: kani-0.63.0...kani-0.64.0 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
1 parent 5b6519b commit 96f7e59

File tree

12 files changed

+41
-20
lines changed

12 files changed

+41
-20
lines changed

CHANGELOG.md

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,27 @@ 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.64.0]
8+
9+
### Major Changes
10+
* Add support for loop modifies in loop contracts by @thanhnguyen-aws in https://github.com/model-checking/kani/pull/4174
11+
* Autoharness: Derive `Arbitrary` for structs and enums by @carolynzech in https://github.com/model-checking/kani/pull/4167, https://github.com/model-checking/kani/pull/4194
12+
* Remove `assess` subcommand by @carolynzech in https://github.com/model-checking/kani/pull/4111
13+
14+
### What's Changed
15+
* Fix static union value crash by @thanhnguyen-aws in https://github.com/model-checking/kani/pull/4112
16+
* Fix loop invariant historical variables bug by @thanhnguyen-aws in https://github.com/model-checking/kani/pull/4150
17+
* Update quantifiers' documentation by @thanhnguyen-aws in https://github.com/model-checking/kani/pull/4142
18+
* Optimize goto binary exporting in `cprover_bindings` by @AlexanderPortland in https://github.com/model-checking/kani/pull/4148
19+
* Add the option to generate performance flamegraphs by @AlexanderPortland in https://github.com/model-checking/kani/pull/4138
20+
* Introduce compiler timing script & CI job by @AlexanderPortland in https://github.com/model-checking/kani/pull/4154
21+
* Optimize reachability with non-mutating global passes by @AlexanderPortland in https://github.com/model-checking/kani/pull/4177
22+
* Stub panics during MIR transformation by @AlexanderPortland in https://github.com/model-checking/kani/pull/4169
23+
* BoundedArbitrary: Handle enums with zero or one variants by @zhassan-aws in https://github.com/model-checking/kani/pull/4171
24+
* Upgrade toolchain to 2025-07-02 by @carolynzech, @tautschnig in https://github.com/model-checking/kani/pull/4195
25+
26+
**Full Changelog**: https://github.com/model-checking/kani/compare/kani-0.63.0...kani-0.64.0
27+
728
## [0.63.0]
829

930
### Breaking Changes

Cargo.lock

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -203,7 +203,7 @@ dependencies = [
203203

204204
[[package]]
205205
name = "build-kani"
206-
version = "0.63.0"
206+
version = "0.64.0"
207207
dependencies = [
208208
"anyhow",
209209
"cargo_metadata",
@@ -464,7 +464,7 @@ checksum = "773648b94d0e5d620f64f280777445740e61fe701025087ec8b57f45c791888b"
464464

465465
[[package]]
466466
name = "cprover_bindings"
467-
version = "0.63.0"
467+
version = "0.64.0"
468468
dependencies = [
469469
"fxhash",
470470
"lazy_static",
@@ -1079,15 +1079,15 @@ dependencies = [
10791079

10801080
[[package]]
10811081
name = "kani"
1082-
version = "0.63.0"
1082+
version = "0.64.0"
10831083
dependencies = [
10841084
"kani_core",
10851085
"kani_macros",
10861086
]
10871087

10881088
[[package]]
10891089
name = "kani-compiler"
1090-
version = "0.63.0"
1090+
version = "0.64.0"
10911091
dependencies = [
10921092
"charon",
10931093
"clap",
@@ -1125,7 +1125,7 @@ dependencies = [
11251125

11261126
[[package]]
11271127
name = "kani-driver"
1128-
version = "0.63.0"
1128+
version = "0.64.0"
11291129
dependencies = [
11301130
"anyhow",
11311131
"cargo_metadata",
@@ -1155,7 +1155,7 @@ dependencies = [
11551155

11561156
[[package]]
11571157
name = "kani-verifier"
1158-
version = "0.63.0"
1158+
version = "0.64.0"
11591159
dependencies = [
11601160
"anyhow",
11611161
"home",
@@ -1164,14 +1164,14 @@ dependencies = [
11641164

11651165
[[package]]
11661166
name = "kani_core"
1167-
version = "0.63.0"
1167+
version = "0.64.0"
11681168
dependencies = [
11691169
"kani_macros",
11701170
]
11711171

11721172
[[package]]
11731173
name = "kani_macros"
1174-
version = "0.63.0"
1174+
version = "0.64.0"
11751175
dependencies = [
11761176
"proc-macro-error2",
11771177
"proc-macro2",
@@ -1181,7 +1181,7 @@ dependencies = [
11811181

11821182
[[package]]
11831183
name = "kani_metadata"
1184-
version = "0.63.0"
1184+
version = "0.64.0"
11851185
dependencies = [
11861186
"clap",
11871187
"cprover_bindings",
@@ -1993,7 +1993,7 @@ dependencies = [
19931993

19941994
[[package]]
19951995
name = "std"
1996-
version = "0.63.0"
1996+
version = "0.64.0"
19971997
dependencies = [
19981998
"kani",
19991999
]

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.63.0"
6+
version = "0.64.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.63.0"
6+
version = "0.64.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.63.0"
6+
version = "0.64.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.63.0"
6+
version = "0.64.0"
77
edition = "2021"
88
description = "Build a project with Kani and run all proof harnesses"
99
license = "MIT OR Apache-2.0"

kani_metadata/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_metadata"
6-
version = "0.63.0"
6+
version = "0.64.0"
77
edition = "2021"
88
license = "MIT OR Apache-2.0"
99
publish = false

library/kani/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"
6-
version = "0.63.0"
6+
version = "0.64.0"
77
edition = "2021"
88
license = "MIT OR Apache-2.0"
99
publish = false

library/kani_core/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_core"
6-
version = "0.63.0"
6+
version = "0.64.0"
77
edition = "2021"
88
license = "MIT OR Apache-2.0"
99
publish = false

library/kani_macros/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_macros"
6-
version = "0.63.0"
6+
version = "0.64.0"
77
edition = "2021"
88
license = "MIT OR Apache-2.0"
99
publish = false

0 commit comments

Comments
 (0)