Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
21 changes: 21 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,27 @@ 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.64.0]

### Major Changes
* Add support for loop modifies in loop contracts by @thanhnguyen-aws in https://github.com/model-checking/kani/pull/4174
* 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
* Remove `assess` subcommand by @carolynzech in https://github.com/model-checking/kani/pull/4111

### What's Changed
* Fix static union value crash by @thanhnguyen-aws in https://github.com/model-checking/kani/pull/4112
* Fix loop invariant historical variables bug by @thanhnguyen-aws in https://github.com/model-checking/kani/pull/4150
* Update quantifiers' documentation by @thanhnguyen-aws in https://github.com/model-checking/kani/pull/4142
* Optimize goto binary exporting in `cprover_bindings` by @AlexanderPortland in https://github.com/model-checking/kani/pull/4148
* Add the option to generate performance flamegraphs by @AlexanderPortland in https://github.com/model-checking/kani/pull/4138
* Introduce compiler timing script & CI job by @AlexanderPortland in https://github.com/model-checking/kani/pull/4154
* Optimize reachability with non-mutating global passes by @AlexanderPortland in https://github.com/model-checking/kani/pull/4177
* Stub panics during MIR transformation by @AlexanderPortland in https://github.com/model-checking/kani/pull/4169
* BoundedArbitrary: Handle enums with zero or one variants by @zhassan-aws in https://github.com/model-checking/kani/pull/4171
* Upgrade toolchain to 2025-07-02 by @carolynzech, @tautschnig in https://github.com/model-checking/kani/pull/4195

**Full Changelog**: https://github.com/model-checking/kani/compare/kani-0.63.0...kani-0.64.0

## [0.63.0]

### Breaking Changes
Expand Down
20 changes: 10 additions & 10 deletions Cargo.lock
Original file line number Diff line number Diff line change
Expand Up @@ -203,7 +203,7 @@ dependencies = [

[[package]]
name = "build-kani"
version = "0.63.0"
version = "0.64.0"
dependencies = [
"anyhow",
"cargo_metadata",
Expand Down Expand Up @@ -464,7 +464,7 @@ checksum = "773648b94d0e5d620f64f280777445740e61fe701025087ec8b57f45c791888b"

[[package]]
name = "cprover_bindings"
version = "0.63.0"
version = "0.64.0"
dependencies = [
"fxhash",
"lazy_static",
Expand Down Expand Up @@ -1079,15 +1079,15 @@ dependencies = [

[[package]]
name = "kani"
version = "0.63.0"
version = "0.64.0"
dependencies = [
"kani_core",
"kani_macros",
]

[[package]]
name = "kani-compiler"
version = "0.63.0"
version = "0.64.0"
dependencies = [
"charon",
"clap",
Expand Down Expand Up @@ -1125,7 +1125,7 @@ dependencies = [

[[package]]
name = "kani-driver"
version = "0.63.0"
version = "0.64.0"
dependencies = [
"anyhow",
"cargo_metadata",
Expand Down Expand Up @@ -1155,7 +1155,7 @@ dependencies = [

[[package]]
name = "kani-verifier"
version = "0.63.0"
version = "0.64.0"
dependencies = [
"anyhow",
"home",
Expand All @@ -1164,14 +1164,14 @@ dependencies = [

[[package]]
name = "kani_core"
version = "0.63.0"
version = "0.64.0"
dependencies = [
"kani_macros",
]

[[package]]
name = "kani_macros"
version = "0.63.0"
version = "0.64.0"
dependencies = [
"proc-macro-error2",
"proc-macro2",
Expand All @@ -1181,7 +1181,7 @@ dependencies = [

[[package]]
name = "kani_metadata"
version = "0.63.0"
version = "0.64.0"
dependencies = [
"clap",
"cprover_bindings",
Expand Down Expand Up @@ -1993,7 +1993,7 @@ dependencies = [

[[package]]
name = "std"
version = "0.63.0"
version = "0.64.0"
dependencies = [
"kani",
]
Expand Down
2 changes: 1 addition & 1 deletion Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@

[package]
name = "kani-verifier"
version = "0.63.0"
version = "0.64.0"
edition = "2021"
description = "A bit-precise model checker for Rust."
readme = "README.md"
Expand Down
2 changes: 1 addition & 1 deletion cprover_bindings/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@

[package]
name = "cprover_bindings"
version = "0.63.0"
version = "0.64.0"
edition = "2021"
license = "MIT OR Apache-2.0"
publish = false
Expand Down
2 changes: 1 addition & 1 deletion kani-compiler/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@

[package]
name = "kani-compiler"
version = "0.63.0"
version = "0.64.0"
edition = "2021"
license = "MIT OR Apache-2.0"
publish = false
Expand Down
2 changes: 1 addition & 1 deletion kani-driver/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@

[package]
name = "kani-driver"
version = "0.63.0"
version = "0.64.0"
edition = "2021"
description = "Build a project with Kani and run all proof harnesses"
license = "MIT OR Apache-2.0"
Expand Down
2 changes: 1 addition & 1 deletion kani_metadata/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@

[package]
name = "kani_metadata"
version = "0.63.0"
version = "0.64.0"
edition = "2021"
license = "MIT OR Apache-2.0"
publish = false
Expand Down
2 changes: 1 addition & 1 deletion library/kani/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@

[package]
name = "kani"
version = "0.63.0"
version = "0.64.0"
edition = "2021"
license = "MIT OR Apache-2.0"
publish = false
Expand Down
2 changes: 1 addition & 1 deletion library/kani_core/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@

[package]
name = "kani_core"
version = "0.63.0"
version = "0.64.0"
edition = "2021"
license = "MIT OR Apache-2.0"
publish = false
Expand Down
2 changes: 1 addition & 1 deletion library/kani_macros/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@

[package]
name = "kani_macros"
version = "0.63.0"
version = "0.64.0"
edition = "2021"
license = "MIT OR Apache-2.0"
publish = false
Expand Down
2 changes: 1 addition & 1 deletion library/std/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -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.63.0"
version = "0.64.0"
edition = "2021"
license = "MIT OR Apache-2.0"
publish = false
Expand Down
2 changes: 1 addition & 1 deletion tools/build-kani/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@

[package]
name = "build-kani"
version = "0.63.0"
version = "0.64.0"
edition = "2021"
description = "Builds Kani, Sysroot and release bundle."
license = "MIT OR Apache-2.0"
Expand Down
Loading