Merge branch 'main' into features/loop-contracts-annotation

.github/workflows/cargo-update.yml

@@ -37,7 +37,7 @@ jobs:
  git diff
  fi
  - name: Create Pull Request
- uses: peter-evans/create-pull-request@v6
+ uses: peter-evans/create-pull-request@v7
  with:
  commit-message: Upgrade cargo dependencies to ${{ env.today }}
  branch: cargo-update-${{ env.today }}

.github/workflows/cbmc-latest.yml

@@ -87,7 +87,7 @@ jobs:
  - name: Build CBMC
  working-directory: ./cbmc
  run: |
- cmake -S . -Bbuild -DWITH_JBMC=OFF
+ cmake -S . -Bbuild -DWITH_JBMC=OFF -Dsat_impl="minisat2;cadical"
  cmake --build build -- -j 4
  # Prepend the bin directory to $PATH
  echo "${GITHUB_WORKSPACE}/cbmc/build/bin" >> $GITHUB_PATH

.github/workflows/cbmc-update.yml

@@ -63,7 +63,7 @@ jobs:
 
  - name: Create Pull Request
  if: ${{ env.next_step == 'create_pr' }}
- uses: peter-evans/create-pull-request@v6
+ uses: peter-evans/create-pull-request@v7
  with:
  commit-message: Upgrade CBMC from ${{ env.CBMC_VERSION }} to ${{ env.CBMC_LATEST }}
  branch: cbmc-${{ env.CBMC_LATEST }}

.github/workflows/toolchain-upgrade.yml

@@ -38,7 +38,7 @@ jobs:
  - name: Create Pull Request
  id: create_pr
  if: ${{ env.next_step == 'create_pr' }}
- uses: peter-evans/create-pull-request@v6
+ uses: peter-evans/create-pull-request@v7
  with:
  commit-message: Upgrade Rust toolchain to nightly-${{ env.next_toolchain_date }}
  branch: toolchain-${{ env.next_toolchain_date }}

CHANGELOG.md

@@ -4,6 +4,28 @@ 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.55.0]
+
+### Major/Breaking Changes
+* Coverage reporting in Kani is now source-based instead of line-based.
+Consequently, the unstable `-Zline-coverage` flag has been replaced with a `-Zsource-coverage` one.
+Check the [Source-Coverage RFC](https://model-checking.github.io/kani/rfc/rfcs/0011-source-coverage.html) for more details.
+* Several improvements were made to the memory initialization checks. The current state is summarized in https://github.com/model-checking/kani/issues/3300. We welcome your feedback!
+
+### What's Changed
+* Update CBMC build instructions for Amazon Linux 2 by @tautschnig in https://github.com/model-checking/kani/pull/3431
+* Implement memory initialization state copy functionality by @artemagvanian in https://github.com/model-checking/kani/pull/3350
+* Make points-to analysis handle all intrinsics explicitly by @artemagvanian in https://github.com/model-checking/kani/pull/3452
+* Avoid corner-cases by grouping instrumentation into basic blocks and using backward iteration by @artemagvanian in https://github.com/model-checking/kani/pull/3438
+* Fix ICE due to mishandling of Aggregate rvalue for raw pointers to `str` by @celinval in https://github.com/model-checking/kani/pull/3448
+* Basic support for memory initialization checks for unions by @artemagvanian in https://github.com/model-checking/kani/pull/3444
+* Adopt Rust's source-based code coverage instrumentation by @adpaco-aws in https://github.com/model-checking/kani/pull/3119
+* Extra tests and bug fixes to the delayed UB instrumentation by @artemagvanian in https://github.com/model-checking/kani/pull/3419
+* Partially integrate uninit memory checks into `verify_std` by @artemagvanian in https://github.com/model-checking/kani/pull/3470
+* Rust toolchain upgraded to `nightly-2024-09-03` by @jaisnan @carolynzech 
+
+**Full Changelog**: https://github.com/model-checking/kani/compare/kani-0.54.0...kani-0.55.0
+
 ## [0.54.0]
 
 ### Major Changes

Cargo.lock

@@ -75,9 +75,9 @@ dependencies = [
 
 [[package]]
 name = "anyhow"
-version = "1.0.86"
+version = "1.0.87"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b3d1d046238990b9cf5bcde22a3fb3584ee5cf65fb2765f454ed428c7a0063da"
+checksum = "10f00e1f6e58a40e807377c75c6a7f97bf9044fab57816f2414e6f5f4499d7b8"
 
 [[package]]
 name = "autocfg"
@@ -93,7 +93,7 @@ checksum = "b048fb63fd8b5923fc5aa7b340d8e156aec7ec02f0c78fa8a6ddc2613f6f71de"
 
 [[package]]
 name = "build-kani"
-version = "0.54.0"
+version = "0.55.0"
 dependencies = [
  "anyhow",
  "cargo_metadata",
@@ -147,19 +147,19 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd"
 
 [[package]]
 name = "clap"
-version = "4.5.16"
+version = "4.5.17"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ed6719fffa43d0d87e5fd8caeab59be1554fb028cd30edc88fc4369b17971019"
+checksum = "3e5a21b8495e732f1b3c364c9949b201ca7bae518c502c80256c96ad79eaf6ac"
 dependencies = [
  "clap_builder",
  "clap_derive",
 ]
 
 [[package]]
 name = "clap_builder"
-version = "4.5.15"
+version = "4.5.17"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "216aec2b177652e3846684cbfe25c9964d18ec45234f0f5da5157b207ed1aab6"
+checksum = "8cf2dd12af7a047ad9d6da2b6b249759a22a7abc0f474c1dae1777afa4b21a73"
 dependencies = [
  "anstream",
  "anstyle",
@@ -176,7 +176,7 @@ dependencies = [
  "heck",
  "proc-macro2",
  "quote",
- "syn 2.0.77",
+ "syn",
 ]
 
 [[package]]
@@ -235,7 +235,7 @@ dependencies = [
 
 [[package]]
 name = "cprover_bindings"
-version = "0.54.0"
+version = "0.55.0"
 dependencies = [
  "lazy_static",
  "linear-map",
@@ -459,15 +459,15 @@ checksum = "49f1f14873335454500d59611f1cf4a4b0f786f9ac11f4312a78e4cf2566695b"
 
 [[package]]
 name = "kani"
-version = "0.54.0"
+version = "0.55.0"
 dependencies = [
  "kani_core",
  "kani_macros",
 ]
 
 [[package]]
 name = "kani-compiler"
-version = "0.54.0"
+version = "0.55.0"
 dependencies = [
  "clap",
  "cprover_bindings",
@@ -483,15 +483,15 @@ dependencies = [
  "shell-words",
  "strum",
  "strum_macros",
- "syn 2.0.77",
+ "syn",
  "tracing",
  "tracing-subscriber",
  "tracing-tree",
 ]
 
 [[package]]
 name = "kani-driver"
-version = "0.54.0"
+version = "0.55.0"
 dependencies = [
  "anyhow",
  "cargo_metadata",
@@ -520,7 +520,7 @@ dependencies = [
 
 [[package]]
 name = "kani-verifier"
-version = "0.54.0"
+version = "0.55.0"
 dependencies = [
  "anyhow",
  "home",
@@ -529,24 +529,24 @@ dependencies = [
 
 [[package]]
 name = "kani_core"
-version = "0.54.0"
+version = "0.55.0"
 dependencies = [
  "kani_macros",
 ]
 
 [[package]]
 name = "kani_macros"
-version = "0.54.0"
+version = "0.55.0"
 dependencies = [
- "proc-macro-error",
+ "proc-macro-error2",
  "proc-macro2",
  "quote",
- "syn 2.0.77",
+ "syn",
 ]
 
 [[package]]
 name = "kani_metadata"
-version = "0.54.0"
+version = "0.55.0"
 dependencies = [
  "clap",
  "cprover_bindings",
@@ -801,27 +801,25 @@ dependencies = [
 ]
 
 [[package]]
-name = "proc-macro-error"
-version = "1.0.4"
+name = "proc-macro-error-attr2"
+version = "2.0.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "da25490ff9892aab3fcf7c36f08cfb902dd3e71ca0f9f9517bea02a73a5ce38c"
+checksum = "96de42df36bb9bba5542fe9f1a054b8cc87e172759a1868aa05c1f3acc89dfc5"
 dependencies = [
- "proc-macro-error-attr",
  "proc-macro2",
  "quote",
- "syn 1.0.109",
- "version_check",
 ]
 
 [[package]]
-name = "proc-macro-error-attr"
-version = "1.0.4"
+name = "proc-macro-error2"
+version = "2.0.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "a1be40180e52ecc98ad80b184934baf3d0d29f979574e439af5a55274b35f869"
+checksum = "11ec05c52be0a07b08061f7dd003e7d7092e0472bc731b4af7bb1ef876109802"
 dependencies = [
+ "proc-macro-error-attr2",
  "proc-macro2",
  "quote",
- "version_check",
+ "syn",
 ]
 
 [[package]]
@@ -953,9 +951,9 @@ checksum = "719b953e2095829ee67db738b3bfa9fa368c94900df327b3f07fe6e794d2fe1f"
 
 [[package]]
 name = "rustix"
-version = "0.38.35"
+version = "0.38.36"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "a85d50532239da68e9addb745ba38ff4612a242c1c7ceea689c4bc7c2f43c36f"
+checksum = "3f55e80d50763938498dd5ebb18647174e0c76dc38c5505294bb224624f30f36"
 dependencies = [
  "bitflags",
  "errno",
@@ -1014,29 +1012,29 @@ dependencies = [
 
 [[package]]
 name = "serde"
-version = "1.0.209"
+version = "1.0.210"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "99fce0ffe7310761ca6bf9faf5115afbc19688edd00171d81b1bb1b116c63e09"
+checksum = "c8e3592472072e6e22e0a54d5904d9febf8508f65fb8552499a1abc7d1078c3a"
 dependencies = [
  "serde_derive",
 ]
 
 [[package]]
 name = "serde_derive"
-version = "1.0.209"
+version = "1.0.210"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "a5831b979fd7b5439637af1752d535ff49f4860c0f341d1baeb6faf0f4242170"
+checksum = "243902eda00fad750862fc144cea25caca5e20d615af0a81bee94ca738f1df1f"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.77",
+ "syn",
 ]
 
 [[package]]
 name = "serde_json"
-version = "1.0.127"
+version = "1.0.128"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "8043c06d9f82bd7271361ed64f415fe5e12a77fdb52e573e7f06a516dea329ad"
+checksum = "6ff5456707a1de34e7e37f2a6fd3d3f808c318259cbd01ab6377795054b483d8"
 dependencies = [
  "itoa",
  "memchr",
@@ -1098,7 +1096,7 @@ checksum = "3c5e1a9a646d36c3599cd173a41282daf47c44583ad367b8e6837255952e5c67"
 
 [[package]]
 name = "std"
-version = "0.54.0"
+version = "0.55.0"
 dependencies = [
  "kani",
 ]
@@ -1136,17 +1134,7 @@ dependencies = [
  "proc-macro2",
  "quote",
  "rustversion",
- "syn 2.0.77",
-]
-
-[[package]]
-name = "syn"
-version = "1.0.109"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "72b64191b275b66ffe2469e8af2c1cfe3bafa67b529ead792a6d0160888b4237"
-dependencies = [
- "proc-macro2",
- "unicode-ident",
+ "syn",
 ]
 
 [[package]]
@@ -1190,7 +1178,7 @@ checksum = "a4558b58466b9ad7ca0f102865eccc95938dca1a74a856f2b57b6629050da261"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.77",
+ "syn",
 ]
 
 [[package]]
@@ -1287,7 +1275,7 @@ checksum = "34704c8d6ebcbc939824180af020566b01a7c01f80641264eba0999f6c2b6be7"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.77",
+ "syn",
 ]
 
 [[package]]
@@ -1574,5 +1562,5 @@ checksum = "fa4f8080344d4671fb4e831a13ad1e68092748387dfc4f55e356242fae12ce3e"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.77",
+ "syn",
 ]

Cargo.toml

@@ -3,7 +3,7 @@
 
 [package]
 name = "kani-verifier"
-version = "0.54.0"
+version = "0.55.0"
 edition = "2021"
 description = "A bit-precise model checker for Rust."
 readme = "README.md"

cprover_bindings/Cargo.toml

@@ -3,7 +3,7 @@
 
 [package]
 name = "cprover_bindings"
-version = "0.54.0"
+version = "0.55.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false

docs/src/SUMMARY.md

@@ -7,6 +7,8 @@
  - [Using Kani](./usage.md)
  - [Verification results](./verification-results.md)
 
+- [Crates Documentation](./crates/index.md)
+
 - [Tutorial](./kani-tutorial.md)
  - [First steps](./tutorial-first-steps.md)
  - [Failures that Kani can spot](./tutorial-kinds-of-failure.md)
@@ -18,6 +20,7 @@
  - [Experimental features](./reference/experimental/experimental-features.md)
  - [Coverage](./reference/experimental/coverage.md)
  - [Stubbing](./reference/experimental/stubbing.md)
+ - [Contracts](./reference/experimental/contracts.md)
  - [Concrete Playback](./reference/experimental/concrete-playback.md)
 - [Application](./application.md)
  - [Comparison with other tools](./tool-comparison.md)
@@ -45,8 +48,6 @@
  - [Unstable features](./rust-feature-support/unstable.md)
  - [Overrides](./overrides.md)
 
-- [Crates Documentation](./crates/index.md)
-
 ---
 
 - [FAQ](./faq.md)

docs/src/getting-started.md

@@ -15,6 +15,7 @@ Proof harnesses are similar to test harnesses, especially property-based test ha
 Kani is currently under active development.
 Releases are published [here](https://github.com/model-checking/kani/releases).
 Major changes to Kani are documented in the [RFC Book](https://model-checking.github.io/kani/rfc).
+We also publish updates on Kani use cases and features on our [blog](https://model-checking.github.io/kani-verifier-blog/).
 
 There is support for a fair amount of Rust language features, but not all (e.g., concurrency).
 Please see [Limitations](./limitations.md) for a detailed list of supported features.