Skip to content

Commit 677c791

Browse files
bump kani vesion 0.65.0 (#4274)
from the autogenerated : ## What's Changed * Ensure that contract closures are FnOnce by @vonaka in #4151 * Adjust sized hierarchy for Kani's memory predicates by @tautschnig in #4193 * Update to Rust edition 2024 by @tautschnig in #4197 * `ptr_offset_from`: Replace arithmetic over pointers by offset arithmetic by @tautschnig in #4180 * Automatic cargo update to 2025-07-07 by @github-actions[bot] in #4208 * Bump tests/perf/s2n-quic from `b8f8cca` to `8715fdf` by @dependabot[bot] in #4209 * Upgrade Rust toolchain to 2025-07-04 by @tautschnig in #4199 * Upgrade Rust toolchain to 2025-07-10 by @thanhnguyen-aws in #4215 * Update CBMC dependency to 6.7.1 by @tautschnig in #4178 * Split compiler flags to avoid dependency recompilation by @AlexanderPortland in #4211 * Fix the bug that assign clause cannot be inferred for the inner loop of nested loops by @thanhnguyen-aws in #4179 * Upgrade Rust toolchain to 2025-07-11 by @thanhnguyen-aws in #4219 * Automatic toolchain upgrade to nightly-2025-07-12 by @github-actions[bot] in #4222 * Fix bug: `goto-cc` crash when there are two quantifers in one proof by @thanhnguyen-aws in #4221 * Automatic toolchain upgrade to nightly-2025-07-13 by @github-actions[bot] in #4223 * Automatic cargo update to 2025-07-14 by @github-actions[bot] in #4224 * Cleanup links to issues that have been addressed by @tautschnig in #4200 * Selectively enable and fix (slow) Tokio tests by @tautschnig in #4203 * Bump tests/perf/s2n-quic from `32ba87d` to `1cbd879` by @dependabot[bot] in #4227 * Implement support for Cargo.toml's default-members by @tautschnig in #4201 * Do not invoke memset with count of zero by @tautschnig in #4205 * Support bitwuzla, cvc5, z3 as solver attribute values by @tautschnig in #4218 * Use CBMC's shuffle_vector expression by @tautschnig in #4204 * Move tests from slow/kani back to regular suite by @tautschnig in #4202 * Automatic toolchain upgrade to nightly-2025-07-14 by @github-actions[bot] in #4225 * Enable GitHub Linux/Arm runners in CI by @tautschnig in #3841 * Automatic cargo update to 2025-07-21 by @github-actions[bot] in #4231 * Skip codegen for unneeded harnesses by @AlexanderPortland in #4213 * Strongly type differing compiler args for clarity by @AlexanderPortland in #4220 * Remove StableMIR ICE workaround by @carolynzech in #4235 * Fix bug: Kani unwinds loops with contract in generic function (with -Z loop-contracts) by @thanhnguyen-aws in #4232 * Automatic cargo update to 2025-07-28 by @github-actions[bot] in #4238 * Bump tests/perf/s2n-quic from `1cbd879` to `4938450` by @dependabot[bot] in #4242 * Upgrade Rust toolchain to 2025-07-21 by @tautschnig in #4241 * Remove `pretty_ty` and use rustc_public's formatter instead by @tautschnig in #4243 * Upgrade Rust toolchain to 2025-07-24 by @tautschnig in #4244 * Documentation cleanup of UB detected by Kani by @tautschnig in #4245 * Upgrade Rust toolchain to 2025-07-29 by @tautschnig in #4247 * Automatic toolchain upgrade to nightly-2025-07-30 by @github-actions[bot] in #4253 * Add unstable option prove-safety-only by @tautschnig in #4239 * Set bits_per_byte in byte_extract expressions by @tautschnig in #4255 * `KaniAttributes` Path Resolution Refactor by @carolynzech in #4249 * Automatic toolchain upgrade to nightly-2025-07-31 by @github-actions[bot] in #4256 * Support contracts & stubs in trait implementations (partial fix) by @carolynzech in #4250 * [Breaking Changes] Remove unstable list feature and default memory checks by @carolynzech in #4258 * Upgrade Rust toolchain to 2025-08-01 by @tautschnig in #4261 * Autoharness: add support for references by @tautschnig in #4234 * Turn off debug assertions under `--prove-safety-only` by @tautschnig in #4262 * Automatic toolchain upgrade to nightly-2025-08-02 by @github-actions[bot] in #4264 * Automatic toolchain upgrade to nightly-2025-08-03 by @github-actions[bot] in #4265 * Automatic cargo update to 2025-08-04 by @github-actions[bot] in #4267 * Automatic toolchain upgrade to nightly-2025-08-04 by @github-actions[bot] in #4266 * Introduce thread pool for writing goto binaries in parallel by @AlexanderPortland in #4236 * Major-version update cargo dependencies by @tautschnig in #4240 * Bump tests/perf/s2n-quic from `4938450` to `8f510f0` by @dependabot[bot] in #4270 * Automatic toolchain upgrade to nightly-2025-08-05 by @github-actions[bot] in #4271 * Automatic toolchain upgrade to nightly-2025-08-06 by @github-actions[bot] in #4272 * Avoid updating irrelevant symbols when handling quantifiers by @AlexanderPortland in #4268 * Lazily evaluate debug info by @AlexanderPortland in #4269 * Clone a template `BodyTransformer` to avoid re-initialization by @AlexanderPortland in #4259 * Ensuring that MIR constants are marked as static consts by @vonaka in #4233 * Fix release job dependencies by @tautschnig in #4273 ## New Contributors * @vonaka made their first contribution in #4151 **Full Changelog**: kani-0.64.0...kani-0.65.0 --------- Co-authored-by: Zyad Hassan <[email protected]>
1 parent 32e3d8f commit 677c791

File tree

12 files changed

+56
-20
lines changed

12 files changed

+56
-20
lines changed

CHANGELOG.md

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,42 @@ 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.65.0]
8+
9+
### Breaking Changes
10+
* Removed unstable list feature and default memory checks by @carolynzech in https://github.com/model-checking/kani/pull/4258
11+
12+
### Major Changes
13+
* Added support for a few SMT solvers (bitwuzla, cvc5, and z3) as solver attribute values (**not** packaged with Kani) by @tautschnig in https://github.com/model-checking/kani/pull/4218
14+
* Improved support for contracts and stubs in trait implementations, expanding verification capabilities for trait-based code by @carolynzech in https://github.com/model-checking/kani/pull/4250
15+
* Added new `--prove-safety-only` option for focused safety verification, allowing you to concentrate on memory safety and undefined behavior detection by @tautschnig in https://github.com/model-checking/kani/pull/4239
16+
* Extended autoharness support to handle references, making it easier to automatically generate verification harnesses by @tautschnig in https://github.com/model-checking/kani/pull/4234
17+
* Multiple performance improvements including parallel goto binary writing, lazy debug info evaluation, and optimized quantifier handling for faster verification times
18+
19+
### What's Changed
20+
* Fixed issue related to the handling of contract closures which was preventing writing contracts for functions that return mutable references by @vonaka in https://github.com/model-checking/kani/pull/4151
21+
* Relaxed the constraint on the pointer type for Kani's memory predicates by @tautschnig in https://github.com/model-checking/kani/pull/4193
22+
* Changed the model for `ptr_offset_from` to enhance verification performance by @tautschnig in https://github.com/model-checking/kani/pull/4180
23+
* Fixed assign clause inference bug for nested loops by @thanhnguyen-aws in https://github.com/model-checking/kani/pull/4179
24+
* Fixed crash when using multiple quantifiers in one proof by @thanhnguyen-aws in https://github.com/model-checking/kani/pull/4221
25+
* Added support for Cargo.toml's default-members configuration by @tautschnig in https://github.com/model-checking/kani/pull/4201
26+
* Improved memset handling to avoid zero-count invocations by @tautschnig in https://github.com/model-checking/kani/pull/4205
27+
* Enhanced safety by disabling debug assertions under prove-safety-only by @tautschnig in https://github.com/model-checking/kani/pull/4262
28+
* Enhanced performance with parallel goto binary writing by @AlexanderPortland in https://github.com/model-checking/kani/pull/4236
29+
* Improved quantifier handling performance by avoiding irrelevant symbol updates by @AlexanderPortland in https://github.com/model-checking/kani/pull/4268
30+
* Enhanced performance with lazy debug info evaluation by @AlexanderPortland in https://github.com/model-checking/kani/pull/4269
31+
* Improved MIR constant handling by marking them as static constants by @vonaka in https://github.com/model-checking/kani/pull/4233
32+
33+
### New Contributors
34+
* @vonaka made their first contribution in https://github.com/model-checking/kani/pull/4151
35+
36+
### Version Updates
37+
* Updated to Rust edition 2024 by @tautschnig in https://github.com/model-checking/kani/pull/4197
38+
* Rust toolchain upgraded to 2025-08-06 by @tautschnig and @thanhnguyen-aws
39+
* Updated CBMC dependency to 6.7.1 by @tautschnig in https://github.com/model-checking/kani/pull/4178
40+
41+
**Full Changelog**: https://github.com/model-checking/kani/compare/kani-0.64.0...kani-0.65.0
42+
743
## [0.64.0]
844

945
### Major 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.64.0"
206+
version = "0.65.0"
207207
dependencies = [
208208
"anyhow",
209209
"cargo_metadata",
@@ -464,7 +464,7 @@ checksum = "773648b94d0e5d620f64f280777445740e61fe701025087ec8b57f45c791888b"
464464

465465
[[package]]
466466
name = "cprover_bindings"
467-
version = "0.64.0"
467+
version = "0.65.0"
468468
dependencies = [
469469
"fxhash",
470470
"lazy_static",
@@ -1090,15 +1090,15 @@ dependencies = [
10901090

10911091
[[package]]
10921092
name = "kani"
1093-
version = "0.64.0"
1093+
version = "0.65.0"
10941094
dependencies = [
10951095
"kani_core",
10961096
"kani_macros",
10971097
]
10981098

10991099
[[package]]
11001100
name = "kani-compiler"
1101-
version = "0.64.0"
1101+
version = "0.65.0"
11021102
dependencies = [
11031103
"charon",
11041104
"clap",
@@ -1136,7 +1136,7 @@ dependencies = [
11361136

11371137
[[package]]
11381138
name = "kani-driver"
1139-
version = "0.64.0"
1139+
version = "0.65.0"
11401140
dependencies = [
11411141
"anyhow",
11421142
"cargo_metadata",
@@ -1166,7 +1166,7 @@ dependencies = [
11661166

11671167
[[package]]
11681168
name = "kani-verifier"
1169-
version = "0.64.0"
1169+
version = "0.65.0"
11701170
dependencies = [
11711171
"anyhow",
11721172
"home",
@@ -1175,14 +1175,14 @@ dependencies = [
11751175

11761176
[[package]]
11771177
name = "kani_core"
1178-
version = "0.64.0"
1178+
version = "0.65.0"
11791179
dependencies = [
11801180
"kani_macros",
11811181
]
11821182

11831183
[[package]]
11841184
name = "kani_macros"
1185-
version = "0.64.0"
1185+
version = "0.65.0"
11861186
dependencies = [
11871187
"proc-macro-error2",
11881188
"proc-macro2",
@@ -1194,7 +1194,7 @@ dependencies = [
11941194

11951195
[[package]]
11961196
name = "kani_metadata"
1197-
version = "0.64.0"
1197+
version = "0.65.0"
11981198
dependencies = [
11991199
"clap",
12001200
"cprover_bindings",
@@ -2013,7 +2013,7 @@ dependencies = [
20132013

20142014
[[package]]
20152015
name = "std"
2016-
version = "0.64.0"
2016+
version = "0.65.0"
20172017
dependencies = [
20182018
"kani",
20192019
]

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.64.0"
6+
version = "0.65.0"
77
edition = "2024"
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.64.0"
6+
version = "0.65.0"
77
edition = "2024"
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.64.0"
6+
version = "0.65.0"
77
edition = "2024"
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.64.0"
6+
version = "0.65.0"
77
edition = "2024"
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.64.0"
6+
version = "0.65.0"
77
edition = "2024"
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.64.0"
6+
version = "0.65.0"
77
edition = "2024"
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.64.0"
6+
version = "0.65.0"
77
edition = "2024"
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.64.0"
6+
version = "0.65.0"
77
edition = "2024"
88
license = "MIT OR Apache-2.0"
99
publish = false

0 commit comments

Comments
 (0)